Theorem ad2ant2r 501

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 471	. 2 |- ( ( ph /\ ( ps /\ ta ) ) -> ch )
3	2	adantlr 469	1 |- ( ( ( ph /\ th ) /\ ( ps /\ ta ) ) -> ch )

Syntax hints:   -> wi 4   /\ wa 103

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

This theorem is referenced by:  foco  5419  fvco4  5557  fliftfun  5763  f1imaen2g  6755  fodju0  7107  mulcomnqg  7320  mulassnqg  7321  ltdcnq  7334  lt2addnq  7341  lt2mulnq  7342  enq0ref  7370  enq0tr  7371  addcmpblnq0  7380  nqpnq0nq  7390  nqnq0m  7392  mulcomnq0  7397  addlocpr  7473  nqprl  7488  nqpru  7489  prmuloc  7503  distrlem1prl  7519  distrlem1pru  7520  ltaddpr  7534  ltexprlemopu  7540  ltexprlemdisj  7543  ltexprlemloc  7544  ltexprlemrl  7547  ltexprlemru  7549  recexprlemloc  7568  recexprlem1ssl  7570  recexprlem1ssu  7571  caucvgprprlemopu  7636  addcomsrg  7692  mulcomsrg  7694  mulasssrg  7695  distrsrg  7696  addcnsr  7771  mulcnsr  7772  addcnsrec  7779  axaddcl  7801  axaddcom  7807  addsub4  8137  muladd  8278  mullt0  8374  apreim  8497  mulge0  8513  divmuldivap  8604  divmul24ap  8608  divmuleqap  8609  recdivap  8610  divadddivap  8619  conjmulap  8621  prodgt0gt0  8742  ltmul12a  8751  lemul12b  8752  lediv2a  8786  qmulcl  9571  irrmul  9581  xrrege0  9757  ge0addcl  9913  ge0mulcl  9914  ge0xaddcl  9915  fzass4  9993  fzrev  10015  fzocatel  10130  expclzaplem  10475  expge0  10487  expge1  10488  lt2sq  10524  le2sq  10525  bernneq  10571  sq11ap  10618  sqrt11ap  10976  2clim  11238  climge0  11262  tanaddaplem  11675  opeo  11830  omeo  11831  cncongr1  12031  pcpremul  12221  pcmul  12229  ennnfonelemf1  12347  setscom  12430  opnneissb  12755  cncnpi  12828  neitx  12868  txcnmpt  12873  txrest  12876  txdis1cn  12878  ptolemy  13345  cxplt3  13440  cxple3  13441  lgslem3  13503  lgsdir2  13534  lgsne0  13539