Theorem ad2ant2r 506

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 476	. 2 |- ( ( ph /\ ( ps /\ ta ) ) -> ch )
3	2	adantlr 474	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  5430  fvco4  5568  fliftfun  5775  f1imaen2g  6771  fodju0  7123  mulcomnqg  7345  mulassnqg  7346  ltdcnq  7359  lt2addnq  7366  lt2mulnq  7367  enq0ref  7395  enq0tr  7396  addcmpblnq0  7405  nqpnq0nq  7415  nqnq0m  7417  mulcomnq0  7422  addlocpr  7498  nqprl  7513  nqpru  7514  prmuloc  7528  distrlem1prl  7544  distrlem1pru  7545  ltaddpr  7559  ltexprlemopu  7565  ltexprlemdisj  7568  ltexprlemloc  7569  ltexprlemrl  7572  ltexprlemru  7574  recexprlemloc  7593  recexprlem1ssl  7595  recexprlem1ssu  7596  caucvgprprlemopu  7661  addcomsrg  7717  mulcomsrg  7719  mulasssrg  7720  distrsrg  7721  addcnsr  7796  mulcnsr  7797  addcnsrec  7804  axaddcl  7826  axaddcom  7832  addsub4  8162  muladd  8303  mullt0  8399  apreim  8522  mulge0  8538  divmuldivap  8629  divmul24ap  8633  divmuleqap  8634  recdivap  8635  divadddivap  8644  conjmulap  8646  prodgt0gt0  8767  ltmul12a  8776  lemul12b  8777  lediv2a  8811  qmulcl  9596  irrmul  9606  xrrege0  9782  ge0addcl  9938  ge0mulcl  9939  ge0xaddcl  9940  fzass4  10018  fzrev  10040  fzocatel  10155  expclzaplem  10500  expge0  10512  expge1  10513  lt2sq  10549  le2sq  10550  bernneq  10596  sq11ap  10643  sqrt11ap  11002  2clim  11264  climge0  11288  tanaddaplem  11701  opeo  11856  omeo  11857  cncongr1  12057  pcpremul  12247  pcmul  12255  ennnfonelemf1  12373  setscom  12456  opnneissb  12949  cncnpi  13022  neitx  13062  txcnmpt  13067  txrest  13070  txdis1cn  13072  ptolemy  13539  cxplt3  13634  cxple3  13635  lgslem3  13697  lgsdir2  13728  lgsne0  13733