Theorem ad2ant2r 509

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

Hypothesis

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

Assertion

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

Proof of Theorem ad2ant2r

Step	Hyp	Ref	Expression
1		ad2ant2.1	. . 3 |- ( ( ph /\ ps ) -> ch )
2	1	adantrr 479	. 2 |- ( ( ph /\ ( ps /\ ta ) ) -> ch )
3	2	adantlr 477	1 |- ( ( ( ph /\ th ) /\ ( ps /\ ta ) ) -> 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:  foco  5491  fvco4  5633  fliftfun  5843  f1imaen2g  6852  fodju0  7213  mulcomnqg  7450  mulassnqg  7451  ltdcnq  7464  lt2addnq  7471  lt2mulnq  7472  enq0ref  7500  enq0tr  7501  addcmpblnq0  7510  nqpnq0nq  7520  nqnq0m  7522  mulcomnq0  7527  addlocpr  7603  nqprl  7618  nqpru  7619  prmuloc  7633  distrlem1prl  7649  distrlem1pru  7650  ltaddpr  7664  ltexprlemopu  7670  ltexprlemdisj  7673  ltexprlemloc  7674  ltexprlemrl  7677  ltexprlemru  7679  recexprlemloc  7698  recexprlem1ssl  7700  recexprlem1ssu  7701  caucvgprprlemopu  7766  addcomsrg  7822  mulcomsrg  7824  mulasssrg  7825  distrsrg  7826  addcnsr  7901  mulcnsr  7902  addcnsrec  7909  axaddcl  7931  axaddcom  7937  addsub4  8269  muladd  8410  mullt0  8507  apreim  8630  mulge0  8646  divmuldivap  8739  divmul24ap  8743  divmuleqap  8744  recdivap  8745  divadddivap  8754  conjmulap  8756  prodgt0gt0  8878  ltmul12a  8887  lemul12b  8888  lediv2a  8922  qmulcl  9711  irrmul  9721  xrrege0  9900  ge0addcl  10056  ge0mulcl  10057  ge0xaddcl  10058  fzass4  10137  fzrev  10159  fzocatel  10275  expclzaplem  10655  expge0  10667  expge1  10668  lt2sq  10705  le2sq  10706  bernneq  10752  sq11ap  10799  sqrt11ap  11203  2clim  11466  climge0  11490  tanaddaplem  11903  opeo  12062  omeo  12063  cncongr1  12271  pcpremul  12462  pcmul  12470  ennnfonelemf1  12635  setscom  12718  dfgrp3mlem  13230  grplactcnv  13234  issubg4m  13323  resgrpisgrp  13325  ghmpreima  13396  ghmeql  13397  conjghm  13406  rngpropd  13511  lmodprop2d  13904  opnneissb  14391  cncnpi  14464  neitx  14504  txcnmpt  14509  txrest  14512  txdis1cn  14514  ptolemy  15060  cxplt3  15156  cxple3  15157  lgslem3  15243  lgsdir2  15274  lgsne0  15279  lgsquad3  15325