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  5460  fvco4  5601  fliftfun  5810  f1imaen2g  6807  fodju0  7159  mulcomnqg  7396  mulassnqg  7397  ltdcnq  7410  lt2addnq  7417  lt2mulnq  7418  enq0ref  7446  enq0tr  7447  addcmpblnq0  7456  nqpnq0nq  7466  nqnq0m  7468  mulcomnq0  7473  addlocpr  7549  nqprl  7564  nqpru  7565  prmuloc  7579  distrlem1prl  7595  distrlem1pru  7596  ltaddpr  7610  ltexprlemopu  7616  ltexprlemdisj  7619  ltexprlemloc  7620  ltexprlemrl  7623  ltexprlemru  7625  recexprlemloc  7644  recexprlem1ssl  7646  recexprlem1ssu  7647  caucvgprprlemopu  7712  addcomsrg  7768  mulcomsrg  7770  mulasssrg  7771  distrsrg  7772  addcnsr  7847  mulcnsr  7848  addcnsrec  7855  axaddcl  7877  axaddcom  7883  addsub4  8214  muladd  8355  mullt0  8451  apreim  8574  mulge0  8590  divmuldivap  8683  divmul24ap  8687  divmuleqap  8688  recdivap  8689  divadddivap  8698  conjmulap  8700  prodgt0gt0  8822  ltmul12a  8831  lemul12b  8832  lediv2a  8866  qmulcl  9651  irrmul  9661  xrrege0  9839  ge0addcl  9995  ge0mulcl  9996  ge0xaddcl  9997  fzass4  10076  fzrev  10098  fzocatel  10213  expclzaplem  10558  expge0  10570  expge1  10571  lt2sq  10608  le2sq  10609  bernneq  10655  sq11ap  10702  sqrt11ap  11061  2clim  11323  climge0  11347  tanaddaplem  11760  opeo  11916  omeo  11917  cncongr1  12117  pcpremul  12307  pcmul  12315  ennnfonelemf1  12433  setscom  12516  dfgrp3mlem  12995  grplactcnv  12999  issubg4m  13085  resgrpisgrp  13087  rngpropd  13207  lmodprop2d  13537  opnneissb  13951  cncnpi  14024  neitx  14064  txcnmpt  14069  txrest  14072  txdis1cn  14074  ptolemy  14541  cxplt3  14636  cxple3  14637  lgslem3  14699  lgsdir2  14730  lgsne0  14735