Theorem 3adantl2 1218

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

Hypothesis

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

Assertion

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

Proof of Theorem 3adantl2

Step	Hyp	Ref	Expression
1		3simpb 1059	. 2 |- ( ( ph /\ ta /\ ps ) -> ( ph /\ ps ) )
2		3adantl.1	. 2 |- ( ( ( ph /\ ps ) /\ ch ) -> th )
3	1, 2	sylan 488	1 |- ( ( ( ph /\ ta /\ ps ) /\ 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:  3ad2antl1  1223  omord2  7647  nnmord  7712  axcc3  9260  lediv2a  10917  zdiv  11447  clatleglb  17126  mulgnn0subcl  17554  mulgsubcl  17555  ghmmulg  17672  obs2ss  20073  scmatf1  20337  neiint  20908  cnpnei  21068  caublcls  23107  axlowdimlem16  25837  clwwlksext2edg  26923  ipval2lem2  27559  fh1  28477  cm2j  28479  hoadddi  28662  hoadddir  28663  lautco  35383  supxrge  39554  infleinflem2  39587  stoweidlem44  40261  fourierdlem41  40365  fourierdlem42  40366  fourierdlem54  40377  fourierdlem83  40406  sge0uzfsumgt  40661