Theorem ad2ant2l 508

Description: Deduction adding two conjuncts to antecedent. (Contributed by NM, 8-Jan-2006.)

Hypothesis

Ref	Expression
ad2ant2.1	|- ( ( ph /\ ps ) -> ch )

Assertion

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

Proof of Theorem ad2ant2l

Step	Hyp	Ref	Expression
1		ad2ant2.1	. . 3 |- ( ( ph /\ ps ) -> ch )
2	1	adantrl 478	. 2 |- ( ( ph /\ ( ta /\ ps ) ) -> ch )
3	2	adantll 476	1 |- ( ( ( th /\ ph ) /\ ( ta /\ ps ) ) -> ch )

Syntax hints:   -> wi 4   /\ wa 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem is referenced by:  mpteqb  5655  mpofun  6028  xpdom2  6899  addcmpblnq  7451  addpipqqslem  7453  addpipqqs  7454  addclnq  7459  addcomnqg  7465  addassnqg  7466  mulcomnqg  7467  mulassnqg  7468  distrnqg  7471  ltdcnq  7481  enq0ref  7517  addcmpblnq0  7527  addclnq0  7535  nqpnq0nq  7537  nqnq0a  7538  nqnq0m  7539  distrnq0  7543  mulcomnq0  7544  addassnq0lemcl  7545  genpdisj  7607  appdiv0nq  7648  addcomsrg  7839  mulcomsrg  7841  mulasssrg  7842  distrsrg  7843  addcnsr  7918  mulcnsr  7919  addcnsrec  7926  axaddcl  7948  axmulcl  7950  axaddcom  7954  add42  8205  muladd  8427  mulsub  8444  apreim  8647  divmuleqap  8761  ltmul12a  8904  lemul12b  8905  lemul12a  8906  qaddcl  9726  qmulcl  9728  iooshf  10044  fzass4  10154  elfzomelpfzo  10324  tanaddaplem  11920  issubg4m  13399  ghmpreima  13472  islmodd  13925  opnneissb  14475  neitx  14588  txcnmpt  14593  txrest  14596  metcnp3  14831  cncfmet  14912  dveflem  15046  lgsdir2  15358