Theorem 3ad2antl2 1224

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

Hypothesis

Ref	Expression
3ad2antl.1	|- ( ( ph /\ ch ) -> th )

Assertion

Ref	Expression
3ad2antl2	|- ( ( ( ps /\ ph /\ ta ) /\ ch ) -> th )

Proof of Theorem 3ad2antl2

Step	Hyp	Ref	Expression
1		3ad2antl.1	. . 3 |- ( ( ph /\ ch ) -> th )
2	1	adantlr 751	. 2 |- ( ( ( ph /\ ta ) /\ ch ) -> th )
3	2	3adantl1 1217	1 |- ( ( ( ps /\ ph /\ ta ) /\ ch ) -> th )

Syntax hints:   -> wi 4   /\ wa 384   /\ w3a 1037

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 197  df-an 386  df-3an 1039

This theorem is referenced by:  fcofo  6543  cocan1  6546  ordiso2  8420  fin1a2lem9  9230  fin1a2lem12  9233  gchpwdom  9492  winainflem  9515  bpolydif  14786  muldvds1  15006  lcmdvds  15321  ramcl  15733  gsumccat  17378  oddvdsnn0  17963  ghmplusg  18249  frlmsslss2  20114  frlmsslsp  20135  islindf4  20177  mamures  20196  matepmcl  20268  matepm2cl  20269  pmatcollpw2lem  20582  cnpnei  21068  ssref  21315  qtopss  21518  elfm2  21752  flffbas  21799  cnpfcf  21845  deg1ldg  23852  brbtwn2  25785  colinearalg  25790  axsegconlem1  25797  upgrpredgv  26034  cusgrrusgr  26477  upgrewlkle2  26502  wwlksm1edg  26767  clwwlksf  26915  nvmul0or  27505  hoadddi  28662  volfiniune  30293  bnj548  30967  funsseq  31666  nn0prpwlem  32317  fnemeet1  32361  curfv  33389  keridl  33831  pmapglbx  35055  elpaddn0  35086  paddasslem9  35114  paddasslem10  35115  cdleme42mgN  35776  relexpxpmin  38009  ntrclsk3  38368  n0p  39209  wessf1ornlem  39371  infxr  39583  lptre2pt  39872  dvnprodlem1  40161  fourierdlem42  40366  fourierdlem48  40371  fourierdlem54  40377  fourierdlem77  40400  sge0rpcpnf  40638  hoicvr  40762  smflimsuplem7  41032