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:  fundif  5337  foco  5531  fvco4  5674  fliftfun  5888  f1imaen2g  6908  fodju0  7275  mulcomnqg  7531  mulassnqg  7532  ltdcnq  7545  lt2addnq  7552  lt2mulnq  7553  enq0ref  7581  enq0tr  7582  addcmpblnq0  7591  nqpnq0nq  7601  nqnq0m  7603  mulcomnq0  7608  addlocpr  7684  nqprl  7699  nqpru  7700  prmuloc  7714  distrlem1prl  7730  distrlem1pru  7731  ltaddpr  7745  ltexprlemopu  7751  ltexprlemdisj  7754  ltexprlemloc  7755  ltexprlemrl  7758  ltexprlemru  7760  recexprlemloc  7779  recexprlem1ssl  7781  recexprlem1ssu  7782  caucvgprprlemopu  7847  addcomsrg  7903  mulcomsrg  7905  mulasssrg  7906  distrsrg  7907  addcnsr  7982  mulcnsr  7983  addcnsrec  7990  axaddcl  8012  axaddcom  8018  addsub4  8350  muladd  8491  mullt0  8588  apreim  8711  mulge0  8727  divmuldivap  8820  divmul24ap  8824  divmuleqap  8825  recdivap  8826  divadddivap  8835  conjmulap  8837  prodgt0gt0  8959  ltmul12a  8968  lemul12b  8969  lediv2a  9003  qmulcl  9793  irrmul  9803  xrrege0  9982  ge0addcl  10138  ge0mulcl  10139  ge0xaddcl  10140  fzass4  10219  fzrev  10241  fzocatel  10365  expclzaplem  10745  expge0  10757  expge1  10758  lt2sq  10795  le2sq  10796  bernneq  10842  sq11ap  10889  ccatw2s1p2  11135  swrdccatin2  11220  sqrt11ap  11464  2clim  11727  climge0  11751  tanaddaplem  12164  opeo  12323  omeo  12324  cncongr1  12540  pcpremul  12731  pcmul  12739  ennnfonelemf1  12904  setscom  12987  dfgrp3mlem  13545  grplactcnv  13549  issubg4m  13644  resgrpisgrp  13646  ghmpreima  13717  ghmeql  13718  conjghm  13727  rngpropd  13832  lmodprop2d  14225  opnneissb  14742  cncnpi  14815  neitx  14855  txcnmpt  14860  txrest  14863  txdis1cn  14865  ptolemy  15411  cxplt3  15507  cxple3  15508  lgslem3  15594  lgsdir2  15625  lgsne0  15630  lgsquad3  15676