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  5365  foco  5559  fvco4  5706  fliftfun  5920  f1imaen2g  6945  fodju0  7314  mulcomnqg  7570  mulassnqg  7571  ltdcnq  7584  lt2addnq  7591  lt2mulnq  7592  enq0ref  7620  enq0tr  7621  addcmpblnq0  7630  nqpnq0nq  7640  nqnq0m  7642  mulcomnq0  7647  addlocpr  7723  nqprl  7738  nqpru  7739  prmuloc  7753  distrlem1prl  7769  distrlem1pru  7770  ltaddpr  7784  ltexprlemopu  7790  ltexprlemdisj  7793  ltexprlemloc  7794  ltexprlemrl  7797  ltexprlemru  7799  recexprlemloc  7818  recexprlem1ssl  7820  recexprlem1ssu  7821  caucvgprprlemopu  7886  addcomsrg  7942  mulcomsrg  7944  mulasssrg  7945  distrsrg  7946  addcnsr  8021  mulcnsr  8022  addcnsrec  8029  axaddcl  8051  axaddcom  8057  addsub4  8389  muladd  8530  mullt0  8627  apreim  8750  mulge0  8766  divmuldivap  8859  divmul24ap  8863  divmuleqap  8864  recdivap  8865  divadddivap  8874  conjmulap  8876  prodgt0gt0  8998  ltmul12a  9007  lemul12b  9008  lediv2a  9042  qmulcl  9832  irrmul  9842  xrrege0  10021  ge0addcl  10177  ge0mulcl  10178  ge0xaddcl  10179  fzass4  10258  fzrev  10280  fzocatel  10405  expclzaplem  10785  expge0  10797  expge1  10798  lt2sq  10835  le2sq  10836  bernneq  10882  sq11ap  10929  ccatw2s1p2  11176  swrdccatin2  11261  sqrt11ap  11549  2clim  11812  climge0  11836  tanaddaplem  12249  opeo  12408  omeo  12409  cncongr1  12625  pcpremul  12816  pcmul  12824  ennnfonelemf1  12989  setscom  13072  dfgrp3mlem  13631  grplactcnv  13635  issubg4m  13730  resgrpisgrp  13732  ghmpreima  13803  ghmeql  13804  conjghm  13813  rngpropd  13918  lmodprop2d  14312  opnneissb  14829  cncnpi  14902  neitx  14942  txcnmpt  14947  txrest  14950  txdis1cn  14952  ptolemy  15498  cxplt3  15594  cxple3  15595  lgslem3  15681  lgsdir2  15712  lgsne0  15717  lgsquad3  15763  umgr2edg  16005  umgrvad2edg  16009  wlkeq  16065