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  5407  foco  5608  fvco4  5756  fliftfun  5977  f1imaen2g  7048  fodju0  7453  mulcomnqg  7716  mulassnqg  7717  ltdcnq  7730  lt2addnq  7737  lt2mulnq  7738  enq0ref  7766  enq0tr  7767  addcmpblnq0  7776  nqpnq0nq  7786  nqnq0m  7788  mulcomnq0  7793  addlocpr  7869  nqprl  7884  nqpru  7885  prmuloc  7899  distrlem1prl  7915  distrlem1pru  7916  ltaddpr  7930  ltexprlemopu  7936  ltexprlemdisj  7939  ltexprlemloc  7940  ltexprlemrl  7943  ltexprlemru  7945  recexprlemloc  7964  recexprlem1ssl  7966  recexprlem1ssu  7967  caucvgprprlemopu  8032  addcomsrg  8088  mulcomsrg  8090  mulasssrg  8091  distrsrg  8092  addcnsr  8167  mulcnsr  8168  addcnsrec  8175  axaddcl  8197  axaddcom  8203  addsub4  8535  muladd  8677  mullt0  8774  apreim  8897  mulge0  8913  divmuldivap  9008  divmul24ap  9012  divmuleqap  9013  recdivap  9014  divadddivap  9023  conjmulap  9025  prodgt0gt0  9147  ltmul12a  9156  lemul12b  9157  lediv2a  9191  qmulcl  9992  irrmul  10002  xrrege0  10182  ge0addcl  10338  ge0mulcl  10339  ge0xaddcl  10340  fzass4  10422  fzrev  10445  fzocatel  10571  expclzaplem  10954  expge0  10966  expge1  10967  lt2sq  11004  le2sq  11005  bernneq  11052  sq11ap  11099  ccatw2s1p1g  11363  ccatw2s1p2  11364  swrdccatin2  11451  sqrt11ap  11754  2clim  12017  climge0  12041  tanaddaplem  12455  opeo  12614  omeo  12615  cncongr1  12831  pcpremul  13022  pcmul  13030  ennnfonelemf1  13259  setscom  13342  dfgrp3mlem  13852  grplactcnv  13856  issubg4m  13945  resgrpisgrp  13947  ghmpreima  14018  ghmeql  14019  conjghm  14028  rngpropd  14201  lmodprop2d  14629  opnneissb  15151  cncnpi  15224  neitx  15264  txcnmpt  15269  txrest  15272  txdis1cn  15274  ptolemy  15820  cxplt3  15916  cxple3  15917  lgslem3  16006  lgsdir2  16037  lgsne0  16042  lgsquad3  16088  umgr2edg  16333  umgrvad2edg  16337  wlkeq  16480  clwwlkccatlem  16526