Theorem 3adant3r2 1206

Description: Deduction adding a conjunct to antecedent. (Contributed by NM, 17-Feb-2008.)

Hypothesis

Ref	Expression
3exp.1

Assertion

Ref	Expression
3adant3r2

Proof of Theorem 3adant3r2

Step	Hyp	Ref	Expression
1		3exp.1	. . 3
2	1	3expb 1197	. 2
3	2	3adantr2 1156	1

Syntax hints:  ->wi 4  /\wa 369  /\w3a 973

This theorem is referenced by:  plttr  15600  latjlej2  15696  latmlem1  15711  latmlem2  15712  latledi  15719  latmlej11  15720  latmlej12  15721  ipopos  15790  grppnpcan2  16132  mulgsubdir  16173  imasring  17268  zntoslem  18595  mettri2  20844  mettri  20855  xmetrtri  20858  xmetrtri2  20859  metrtri  20860  grpopnpcan2  25255  grponnncan2  25256  ablomuldiv  25291  ablonnncan1  25297  nvmdi  25545  dipdi  25758  dipassr  25761  dipsubdir  25763  dipsubdi  25764  btwncomim  29663  cgr3tr4  29702  cgr3rflx  29704  colinbtwnle  29768  rngosubdi  30356  rngosubdir  30357  dmncan1  30473  dmncan2  30474  mendlmod  31142  omlfh1N  34983  omlfh3N  34984  cvrnbtwn3  35001  cvrnbtwn4  35004  cvrcmp2  35009  hlatjrot  35097  cvrat3  35166  lplnribN  35275  ltrn2ateq  35905  dvalveclem  36752

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 185  df-an 371  df-3an 975