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  5374  foco  5570  fvco4  5718  fliftfun  5937  f1imaen2g  6967  fodju0  7346  mulcomnqg  7603  mulassnqg  7604  ltdcnq  7617  lt2addnq  7624  lt2mulnq  7625  enq0ref  7653  enq0tr  7654  addcmpblnq0  7663  nqpnq0nq  7673  nqnq0m  7675  mulcomnq0  7680  addlocpr  7756  nqprl  7771  nqpru  7772  prmuloc  7786  distrlem1prl  7802  distrlem1pru  7803  ltaddpr  7817  ltexprlemopu  7823  ltexprlemdisj  7826  ltexprlemloc  7827  ltexprlemrl  7830  ltexprlemru  7832  recexprlemloc  7851  recexprlem1ssl  7853  recexprlem1ssu  7854  caucvgprprlemopu  7919  addcomsrg  7975  mulcomsrg  7977  mulasssrg  7978  distrsrg  7979  addcnsr  8054  mulcnsr  8055  addcnsrec  8062  axaddcl  8084  axaddcom  8090  addsub4  8422  muladd  8563  mullt0  8660  apreim  8783  mulge0  8799  divmuldivap  8892  divmul24ap  8896  divmuleqap  8897  recdivap  8898  divadddivap  8907  conjmulap  8909  prodgt0gt0  9031  ltmul12a  9040  lemul12b  9041  lediv2a  9075  qmulcl  9871  irrmul  9881  xrrege0  10060  ge0addcl  10216  ge0mulcl  10217  ge0xaddcl  10218  fzass4  10297  fzrev  10319  fzocatel  10445  expclzaplem  10826  expge0  10838  expge1  10839  lt2sq  10876  le2sq  10877  bernneq  10923  sq11ap  10970  ccatw2s1p1g  11226  ccatw2s1p2  11227  swrdccatin2  11314  sqrt11ap  11616  2clim  11879  climge0  11903  tanaddaplem  12317  opeo  12476  omeo  12477  cncongr1  12693  pcpremul  12884  pcmul  12892  ennnfonelemf1  13057  setscom  13140  dfgrp3mlem  13699  grplactcnv  13703  issubg4m  13798  resgrpisgrp  13800  ghmpreima  13871  ghmeql  13872  conjghm  13881  rngpropd  13987  lmodprop2d  14381  opnneissb  14898  cncnpi  14971  neitx  15011  txcnmpt  15016  txrest  15019  txdis1cn  15021  ptolemy  15567  cxplt3  15663  cxple3  15664  lgslem3  15750  lgsdir2  15781  lgsne0  15786  lgsquad3  15832  umgr2edg  16077  umgrvad2edg  16081  wlkeq  16224  clwwlkccatlem  16270