Theorem ad2ant2r 513

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 483	. 2 |- ( ( ph /\ ( ps /\ ta ) ) -> ch )
3	2	adantlr 481	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:  fundif  5420  foco  5621  fvco4  5771  fliftfun  5992  f1imaen2g  7070  fodju0  7477  mulcomnqg  7740  mulassnqg  7741  ltdcnq  7754  lt2addnq  7761  lt2mulnq  7762  enq0ref  7790  enq0tr  7791  addcmpblnq0  7800  nqpnq0nq  7810  nqnq0m  7812  mulcomnq0  7817  addlocpr  7893  nqprl  7908  nqpru  7909  prmuloc  7923  distrlem1prl  7939  distrlem1pru  7940  ltaddpr  7954  ltexprlemopu  7960  ltexprlemdisj  7963  ltexprlemloc  7964  ltexprlemrl  7967  ltexprlemru  7969  recexprlemloc  7988  recexprlem1ssl  7990  recexprlem1ssu  7991  caucvgprprlemopu  8056  addcomsrg  8112  mulcomsrg  8114  mulasssrg  8115  distrsrg  8116  addcnsr  8191  mulcnsr  8192  addcnsrec  8199  axaddcl  8221  axaddcom  8227  addsub4  8559  muladd  8701  mullt0  8798  apreim  8921  mulge0  8937  divmuldivap  9032  divmul24ap  9036  divmuleqap  9037  recdivap  9038  divadddivap  9047  conjmulap  9049  prodgt0gt0  9171  ltmul12a  9180  lemul12b  9181  lediv2a  9215  qmulcl  10016  irrmul  10026  xrrege0  10206  ge0addcl  10362  ge0mulcl  10363  ge0xaddcl  10364  fzass4  10446  fzrev  10469  fzocatel  10595  expclzaplem  10978  expge0  10990  expge1  10991  lt2sq  11028  le2sq  11029  bernneq  11076  sq11ap  11123  ccatw2s1p1g  11391  ccatw2s1p2  11392  swrdccatin2  11479  sqrt11ap  11782  2clim  12045  climge0  12069  tanaddaplem  12483  opeo  12642  omeo  12643  cncongr1  12859  pcpremul  13050  pcmul  13058  ennnfonelemf1  13287  setscom  13370  dfgrp3mlem  13880  grplactcnv  13884  issubg4m  13973  resgrpisgrp  13975  ghmpreima  14046  ghmeql  14047  conjghm  14056  rngpropd  14229  lmodprop2d  14657  opnneissb  15179  cncnpi  15252  neitx  15292  txcnmpt  15297  txrest  15300  txdis1cn  15302  ptolemy  15848  cxplt3  15945  cxple3  15946  lgslem3  16035  lgsdir2  16066  lgsne0  16071  lgsquad3  16117  umgr2edg  16362  umgrvad2edg  16366  wlkeq  16509  clwwlkccatlem  16555