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  5319  foco  5511  fvco4  5653  fliftfun  5867  f1imaen2g  6887  fodju0  7251  mulcomnqg  7498  mulassnqg  7499  ltdcnq  7512  lt2addnq  7519  lt2mulnq  7520  enq0ref  7548  enq0tr  7549  addcmpblnq0  7558  nqpnq0nq  7568  nqnq0m  7570  mulcomnq0  7575  addlocpr  7651  nqprl  7666  nqpru  7667  prmuloc  7681  distrlem1prl  7697  distrlem1pru  7698  ltaddpr  7712  ltexprlemopu  7718  ltexprlemdisj  7721  ltexprlemloc  7722  ltexprlemrl  7725  ltexprlemru  7727  recexprlemloc  7746  recexprlem1ssl  7748  recexprlem1ssu  7749  caucvgprprlemopu  7814  addcomsrg  7870  mulcomsrg  7872  mulasssrg  7873  distrsrg  7874  addcnsr  7949  mulcnsr  7950  addcnsrec  7957  axaddcl  7979  axaddcom  7985  addsub4  8317  muladd  8458  mullt0  8555  apreim  8678  mulge0  8694  divmuldivap  8787  divmul24ap  8791  divmuleqap  8792  recdivap  8793  divadddivap  8802  conjmulap  8804  prodgt0gt0  8926  ltmul12a  8935  lemul12b  8936  lediv2a  8970  qmulcl  9760  irrmul  9770  xrrege0  9949  ge0addcl  10105  ge0mulcl  10106  ge0xaddcl  10107  fzass4  10186  fzrev  10208  fzocatel  10330  expclzaplem  10710  expge0  10722  expge1  10723  lt2sq  10760  le2sq  10761  bernneq  10807  sq11ap  10854  ccatw2s1p2  11100  sqrt11ap  11382  2clim  11645  climge0  11669  tanaddaplem  12082  opeo  12241  omeo  12242  cncongr1  12458  pcpremul  12649  pcmul  12657  ennnfonelemf1  12822  setscom  12905  dfgrp3mlem  13463  grplactcnv  13467  issubg4m  13562  resgrpisgrp  13564  ghmpreima  13635  ghmeql  13636  conjghm  13645  rngpropd  13750  lmodprop2d  14143  opnneissb  14660  cncnpi  14733  neitx  14773  txcnmpt  14778  txrest  14781  txdis1cn  14783  ptolemy  15329  cxplt3  15425  cxple3  15426  lgslem3  15512  lgsdir2  15543  lgsne0  15548  lgsquad3  15594