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  5448  fvco4  5588  fliftfun  5796  f1imaen2g  6792  fodju0  7144  mulcomnqg  7381  mulassnqg  7382  ltdcnq  7395  lt2addnq  7402  lt2mulnq  7403  enq0ref  7431  enq0tr  7432  addcmpblnq0  7441  nqpnq0nq  7451  nqnq0m  7453  mulcomnq0  7458  addlocpr  7534  nqprl  7549  nqpru  7550  prmuloc  7564  distrlem1prl  7580  distrlem1pru  7581  ltaddpr  7595  ltexprlemopu  7601  ltexprlemdisj  7604  ltexprlemloc  7605  ltexprlemrl  7608  ltexprlemru  7610  recexprlemloc  7629  recexprlem1ssl  7631  recexprlem1ssu  7632  caucvgprprlemopu  7697  addcomsrg  7753  mulcomsrg  7755  mulasssrg  7756  distrsrg  7757  addcnsr  7832  mulcnsr  7833  addcnsrec  7840  axaddcl  7862  axaddcom  7868  addsub4  8199  muladd  8340  mullt0  8436  apreim  8559  mulge0  8575  divmuldivap  8668  divmul24ap  8672  divmuleqap  8673  recdivap  8674  divadddivap  8683  conjmulap  8685  prodgt0gt0  8807  ltmul12a  8816  lemul12b  8817  lediv2a  8851  qmulcl  9636  irrmul  9646  xrrege0  9824  ge0addcl  9980  ge0mulcl  9981  ge0xaddcl  9982  fzass4  10061  fzrev  10083  fzocatel  10198  expclzaplem  10543  expge0  10555  expge1  10556  lt2sq  10593  le2sq  10594  bernneq  10640  sq11ap  10687  sqrt11ap  11046  2clim  11308  climge0  11332  tanaddaplem  11745  opeo  11901  omeo  11902  cncongr1  12102  pcpremul  12292  pcmul  12300  ennnfonelemf1  12418  setscom  12501  dfgrp3mlem  12967  grplactcnv  12971  issubg4m  13051  resgrpisgrp  13053  opnneissb  13625  cncnpi  13698  neitx  13738  txcnmpt  13743  txrest  13746  txdis1cn  13748  ptolemy  14215  cxplt3  14310  cxple3  14311  lgslem3  14373  lgsdir2  14404  lgsne0  14409