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  5381  foco  5579  fvco4  5727  fliftfun  5947  f1imaen2g  7010  fodju0  7406  mulcomnqg  7663  mulassnqg  7664  ltdcnq  7677  lt2addnq  7684  lt2mulnq  7685  enq0ref  7713  enq0tr  7714  addcmpblnq0  7723  nqpnq0nq  7733  nqnq0m  7735  mulcomnq0  7740  addlocpr  7816  nqprl  7831  nqpru  7832  prmuloc  7846  distrlem1prl  7862  distrlem1pru  7863  ltaddpr  7877  ltexprlemopu  7883  ltexprlemdisj  7886  ltexprlemloc  7887  ltexprlemrl  7890  ltexprlemru  7892  recexprlemloc  7911  recexprlem1ssl  7913  recexprlem1ssu  7914  caucvgprprlemopu  7979  addcomsrg  8035  mulcomsrg  8037  mulasssrg  8038  distrsrg  8039  addcnsr  8114  mulcnsr  8115  addcnsrec  8122  axaddcl  8144  axaddcom  8150  addsub4  8481  muladd  8622  mullt0  8719  apreim  8842  mulge0  8858  divmuldivap  8951  divmul24ap  8955  divmuleqap  8956  recdivap  8957  divadddivap  8966  conjmulap  8968  prodgt0gt0  9090  ltmul12a  9099  lemul12b  9100  lediv2a  9134  qmulcl  9932  irrmul  9942  xrrege0  10121  ge0addcl  10277  ge0mulcl  10278  ge0xaddcl  10279  fzass4  10359  fzrev  10381  fzocatel  10507  expclzaplem  10888  expge0  10900  expge1  10901  lt2sq  10938  le2sq  10939  bernneq  10985  sq11ap  11032  ccatw2s1p1g  11288  ccatw2s1p2  11289  swrdccatin2  11376  sqrt11ap  11678  2clim  11941  climge0  11965  tanaddaplem  12379  opeo  12538  omeo  12539  cncongr1  12755  pcpremul  12946  pcmul  12954  ennnfonelemf1  13119  setscom  13202  dfgrp3mlem  13761  grplactcnv  13765  issubg4m  13860  resgrpisgrp  13862  ghmpreima  13933  ghmeql  13934  conjghm  13943  rngpropd  14049  lmodprop2d  14444  opnneissb  14966  cncnpi  15039  neitx  15079  txcnmpt  15084  txrest  15087  txdis1cn  15089  ptolemy  15635  cxplt3  15731  cxple3  15732  lgslem3  15821  lgsdir2  15852  lgsne0  15857  lgsquad3  15903  umgr2edg  16148  umgrvad2edg  16152  wlkeq  16295  clwwlkccatlem  16341