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  5450  fvco4  5590  fliftfun  5799  f1imaen2g  6795  fodju0  7147  mulcomnqg  7384  mulassnqg  7385  ltdcnq  7398  lt2addnq  7405  lt2mulnq  7406  enq0ref  7434  enq0tr  7435  addcmpblnq0  7444  nqpnq0nq  7454  nqnq0m  7456  mulcomnq0  7461  addlocpr  7537  nqprl  7552  nqpru  7553  prmuloc  7567  distrlem1prl  7583  distrlem1pru  7584  ltaddpr  7598  ltexprlemopu  7604  ltexprlemdisj  7607  ltexprlemloc  7608  ltexprlemrl  7611  ltexprlemru  7613  recexprlemloc  7632  recexprlem1ssl  7634  recexprlem1ssu  7635  caucvgprprlemopu  7700  addcomsrg  7756  mulcomsrg  7758  mulasssrg  7759  distrsrg  7760  addcnsr  7835  mulcnsr  7836  addcnsrec  7843  axaddcl  7865  axaddcom  7871  addsub4  8202  muladd  8343  mullt0  8439  apreim  8562  mulge0  8578  divmuldivap  8671  divmul24ap  8675  divmuleqap  8676  recdivap  8677  divadddivap  8686  conjmulap  8688  prodgt0gt0  8810  ltmul12a  8819  lemul12b  8820  lediv2a  8854  qmulcl  9639  irrmul  9649  xrrege0  9827  ge0addcl  9983  ge0mulcl  9984  ge0xaddcl  9985  fzass4  10064  fzrev  10086  fzocatel  10201  expclzaplem  10546  expge0  10558  expge1  10559  lt2sq  10596  le2sq  10597  bernneq  10643  sq11ap  10690  sqrt11ap  11049  2clim  11311  climge0  11335  tanaddaplem  11748  opeo  11904  omeo  11905  cncongr1  12105  pcpremul  12295  pcmul  12303  ennnfonelemf1  12421  setscom  12504  dfgrp3mlem  12973  grplactcnv  12977  issubg4m  13058  resgrpisgrp  13060  lmodprop2d  13443  opnneissb  13694  cncnpi  13767  neitx  13807  txcnmpt  13812  txrest  13815  txdis1cn  13817  ptolemy  14284  cxplt3  14379  cxple3  14380  lgslem3  14442  lgsdir2  14473  lgsne0  14478