Theorem ad2ant2r 500

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 470	. 2 |- ( ( ph /\ ( ps /\ ta ) ) -> ch )
3	2	adantlr 468	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  5350  fvco4  5486  fliftfun  5690  f1imaen2g  6680  fodju0  7012  mulcomnqg  7184  mulassnqg  7185  ltdcnq  7198  lt2addnq  7205  lt2mulnq  7206  enq0ref  7234  enq0tr  7235  addcmpblnq0  7244  nqpnq0nq  7254  nqnq0m  7256  mulcomnq0  7261  addlocpr  7337  nqprl  7352  nqpru  7353  prmuloc  7367  distrlem1prl  7383  distrlem1pru  7384  ltaddpr  7398  ltexprlemopu  7404  ltexprlemdisj  7407  ltexprlemloc  7408  ltexprlemrl  7411  ltexprlemru  7413  recexprlemloc  7432  recexprlem1ssl  7434  recexprlem1ssu  7435  caucvgprprlemopu  7500  addcomsrg  7556  mulcomsrg  7558  mulasssrg  7559  distrsrg  7560  addcnsr  7635  mulcnsr  7636  addcnsrec  7643  axaddcl  7665  axaddcom  7671  addsub4  7998  muladd  8139  mullt0  8235  apreim  8358  mulge0  8374  divmuldivap  8465  divmul24ap  8469  divmuleqap  8470  recdivap  8471  divadddivap  8480  conjmulap  8482  prodgt0gt0  8602  ltmul12a  8611  lemul12b  8612  lediv2a  8646  qmulcl  9422  irrmul  9432  xrrege0  9601  ge0addcl  9757  ge0mulcl  9758  ge0xaddcl  9759  fzass4  9835  fzrev  9857  fzocatel  9969  expclzaplem  10310  expge0  10322  expge1  10323  lt2sq  10359  le2sq  10360  bernneq  10405  sq11ap  10451  sqrt11ap  10803  2clim  11063  climge0  11087  tanaddaplem  11434  opeo  11583  omeo  11584  cncongr1  11773  ennnfonelemf1  11920  setscom  11988  opnneissb  12313  cncnpi  12386  neitx  12426  txcnmpt  12431  txrest  12434  txdis1cn  12436  ptolemy  12894