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  5363  fvco4  5501  fliftfun  5705  f1imaen2g  6695  fodju0  7027  mulcomnqg  7215  mulassnqg  7216  ltdcnq  7229  lt2addnq  7236  lt2mulnq  7237  enq0ref  7265  enq0tr  7266  addcmpblnq0  7275  nqpnq0nq  7285  nqnq0m  7287  mulcomnq0  7292  addlocpr  7368  nqprl  7383  nqpru  7384  prmuloc  7398  distrlem1prl  7414  distrlem1pru  7415  ltaddpr  7429  ltexprlemopu  7435  ltexprlemdisj  7438  ltexprlemloc  7439  ltexprlemrl  7442  ltexprlemru  7444  recexprlemloc  7463  recexprlem1ssl  7465  recexprlem1ssu  7466  caucvgprprlemopu  7531  addcomsrg  7587  mulcomsrg  7589  mulasssrg  7590  distrsrg  7591  addcnsr  7666  mulcnsr  7667  addcnsrec  7674  axaddcl  7696  axaddcom  7702  addsub4  8029  muladd  8170  mullt0  8266  apreim  8389  mulge0  8405  divmuldivap  8496  divmul24ap  8500  divmuleqap  8501  recdivap  8502  divadddivap  8511  conjmulap  8513  prodgt0gt0  8633  ltmul12a  8642  lemul12b  8643  lediv2a  8677  qmulcl  9456  irrmul  9466  xrrege0  9638  ge0addcl  9794  ge0mulcl  9795  ge0xaddcl  9796  fzass4  9873  fzrev  9895  fzocatel  10007  expclzaplem  10348  expge0  10360  expge1  10361  lt2sq  10397  le2sq  10398  bernneq  10443  sq11ap  10489  sqrt11ap  10842  2clim  11102  climge0  11126  tanaddaplem  11481  opeo  11630  omeo  11631  cncongr1  11820  ennnfonelemf1  11967  setscom  12038  opnneissb  12363  cncnpi  12436  neitx  12476  txcnmpt  12481  txrest  12484  txdis1cn  12486  ptolemy  12953  cxplt3  13048  cxple3  13049