Theorem 3ad2antl2 1159

Description: Deduction adding conjuncts to antecedent. (Contributed by NM, 4-Aug-2007.)

Hypothesis

Ref	Expression
3ad2antl.1

Assertion

Ref	Expression
3ad2antl2

Proof of Theorem 3ad2antl2

Step	Hyp	Ref	Expression
1		3ad2antl.1	. . 3
2	1	adantlr 714	. 2
3	2	3adantl1 1152	1

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

This theorem is referenced by:  fcofo  6191  cocan1  6194  ordiso2  7961  fin1a2lem9  8809  fin1a2lem12  8812  gchpwdom  9069  winainflem  9092  muldvds1  14008  ramcl  14547  gsumccat  16009  oddvdsnn0  16568  ghmplusg  16852  frlmsslss2  18805  frlmsslss2OLD  18806  frlmsslsp  18829  frlmsslspOLD  18830  islindf4  18873  mamures  18892  matepmcl  18964  matepm2cl  18965  pmatcollpw2lem  19278  cnpnei  19765  ssref  20013  qtopss  20216  elfm2  20449  flffbas  20496  cnpfcf  20542  deg1ldg  22492  brbtwn2  24208  colinearalg  24213  axsegconlem1  24220  clwwlkf  24794  2spontn0vne  24887  usgreghash2spot  25069  nvmul0or  25547  hoadddi  26722  volfiniune  28202  funsseq  29199  bpolydif  29817  nn0prpwlem  30140  fnemeet1  30184  keridl  30429  lcmdvds  31214  n0p  31437  lptre2pt  31646  dvnprodlem1  31743  fourierdlem42  31931  fourierdlem48  31937  fourierdlem54  31943  fourierdlem77  31966  spthdifv  32352  bnj548  33955  pmapglbx  35493  elpaddn0  35524  paddasslem9  35552  paddasslem10  35553  cdleme42mgN  36214

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