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:  fundif  5365  foco  5561  fvco4  5708  fliftfun  5926  f1imaen2g  6953  fodju0  7325  mulcomnqg  7581  mulassnqg  7582  ltdcnq  7595  lt2addnq  7602  lt2mulnq  7603  enq0ref  7631  enq0tr  7632  addcmpblnq0  7641  nqpnq0nq  7651  nqnq0m  7653  mulcomnq0  7658  addlocpr  7734  nqprl  7749  nqpru  7750  prmuloc  7764  distrlem1prl  7780  distrlem1pru  7781  ltaddpr  7795  ltexprlemopu  7801  ltexprlemdisj  7804  ltexprlemloc  7805  ltexprlemrl  7808  ltexprlemru  7810  recexprlemloc  7829  recexprlem1ssl  7831  recexprlem1ssu  7832  caucvgprprlemopu  7897  addcomsrg  7953  mulcomsrg  7955  mulasssrg  7956  distrsrg  7957  addcnsr  8032  mulcnsr  8033  addcnsrec  8040  axaddcl  8062  axaddcom  8068  addsub4  8400  muladd  8541  mullt0  8638  apreim  8761  mulge0  8777  divmuldivap  8870  divmul24ap  8874  divmuleqap  8875  recdivap  8876  divadddivap  8885  conjmulap  8887  prodgt0gt0  9009  ltmul12a  9018  lemul12b  9019  lediv2a  9053  qmulcl  9844  irrmul  9854  xrrege0  10033  ge0addcl  10189  ge0mulcl  10190  ge0xaddcl  10191  fzass4  10270  fzrev  10292  fzocatel  10417  expclzaplem  10797  expge0  10809  expge1  10810  lt2sq  10847  le2sq  10848  bernneq  10894  sq11ap  10941  ccatw2s1p2  11192  swrdccatin2  11277  sqrt11ap  11565  2clim  11828  climge0  11852  tanaddaplem  12265  opeo  12424  omeo  12425  cncongr1  12641  pcpremul  12832  pcmul  12840  ennnfonelemf1  13005  setscom  13088  dfgrp3mlem  13647  grplactcnv  13651  issubg4m  13746  resgrpisgrp  13748  ghmpreima  13819  ghmeql  13820  conjghm  13829  rngpropd  13934  lmodprop2d  14328  opnneissb  14845  cncnpi  14918  neitx  14958  txcnmpt  14963  txrest  14966  txdis1cn  14968  ptolemy  15514  cxplt3  15610  cxple3  15611  lgslem3  15697  lgsdir2  15728  lgsne0  15733  lgsquad3  15779  umgr2edg  16021  umgrvad2edg  16025  wlkeq  16100  clwwlkccatlem  16143