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  5445  fvco4  5585  fliftfun  5792  f1imaen2g  6788  fodju0  7140  mulcomnqg  7377  mulassnqg  7378  ltdcnq  7391  lt2addnq  7398  lt2mulnq  7399  enq0ref  7427  enq0tr  7428  addcmpblnq0  7437  nqpnq0nq  7447  nqnq0m  7449  mulcomnq0  7454  addlocpr  7530  nqprl  7545  nqpru  7546  prmuloc  7560  distrlem1prl  7576  distrlem1pru  7577  ltaddpr  7591  ltexprlemopu  7597  ltexprlemdisj  7600  ltexprlemloc  7601  ltexprlemrl  7604  ltexprlemru  7606  recexprlemloc  7625  recexprlem1ssl  7627  recexprlem1ssu  7628  caucvgprprlemopu  7693  addcomsrg  7749  mulcomsrg  7751  mulasssrg  7752  distrsrg  7753  addcnsr  7828  mulcnsr  7829  addcnsrec  7836  axaddcl  7858  axaddcom  7864  addsub4  8194  muladd  8335  mullt0  8431  apreim  8554  mulge0  8570  divmuldivap  8663  divmul24ap  8667  divmuleqap  8668  recdivap  8669  divadddivap  8678  conjmulap  8680  prodgt0gt0  8802  ltmul12a  8811  lemul12b  8812  lediv2a  8846  qmulcl  9631  irrmul  9641  xrrege0  9819  ge0addcl  9975  ge0mulcl  9976  ge0xaddcl  9977  fzass4  10055  fzrev  10077  fzocatel  10192  expclzaplem  10537  expge0  10549  expge1  10550  lt2sq  10586  le2sq  10587  bernneq  10633  sq11ap  10680  sqrt11ap  11038  2clim  11300  climge0  11324  tanaddaplem  11737  opeo  11892  omeo  11893  cncongr1  12093  pcpremul  12283  pcmul  12291  ennnfonelemf1  12409  setscom  12492  dfgrp3mlem  12896  grplactcnv  12900  issubg4m  12979  resgrpisgrp  12981  opnneissb  13437  cncnpi  13510  neitx  13550  txcnmpt  13555  txrest  13558  txdis1cn  13560  ptolemy  14027  cxplt3  14122  cxple3  14123  lgslem3  14185  lgsdir2  14216  lgsne0  14221