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:  foco  5494  fvco4  5636  fliftfun  5846  f1imaen2g  6856  fodju0  7217  mulcomnqg  7455  mulassnqg  7456  ltdcnq  7469  lt2addnq  7476  lt2mulnq  7477  enq0ref  7505  enq0tr  7506  addcmpblnq0  7515  nqpnq0nq  7525  nqnq0m  7527  mulcomnq0  7532  addlocpr  7608  nqprl  7623  nqpru  7624  prmuloc  7638  distrlem1prl  7654  distrlem1pru  7655  ltaddpr  7669  ltexprlemopu  7675  ltexprlemdisj  7678  ltexprlemloc  7679  ltexprlemrl  7682  ltexprlemru  7684  recexprlemloc  7703  recexprlem1ssl  7705  recexprlem1ssu  7706  caucvgprprlemopu  7771  addcomsrg  7827  mulcomsrg  7829  mulasssrg  7830  distrsrg  7831  addcnsr  7906  mulcnsr  7907  addcnsrec  7914  axaddcl  7936  axaddcom  7942  addsub4  8274  muladd  8415  mullt0  8512  apreim  8635  mulge0  8651  divmuldivap  8744  divmul24ap  8748  divmuleqap  8749  recdivap  8750  divadddivap  8759  conjmulap  8761  prodgt0gt0  8883  ltmul12a  8892  lemul12b  8893  lediv2a  8927  qmulcl  9716  irrmul  9726  xrrege0  9905  ge0addcl  10061  ge0mulcl  10062  ge0xaddcl  10063  fzass4  10142  fzrev  10164  fzocatel  10280  expclzaplem  10660  expge0  10672  expge1  10673  lt2sq  10710  le2sq  10711  bernneq  10757  sq11ap  10804  sqrt11ap  11208  2clim  11471  climge0  11495  tanaddaplem  11908  opeo  12067  omeo  12068  cncongr1  12284  pcpremul  12475  pcmul  12483  ennnfonelemf1  12648  setscom  12731  dfgrp3mlem  13277  grplactcnv  13281  issubg4m  13370  resgrpisgrp  13372  ghmpreima  13443  ghmeql  13444  conjghm  13453  rngpropd  13558  lmodprop2d  13951  opnneissb  14438  cncnpi  14511  neitx  14551  txcnmpt  14556  txrest  14559  txdis1cn  14561  ptolemy  15107  cxplt3  15203  cxple3  15204  lgslem3  15290  lgsdir2  15321  lgsne0  15326  lgsquad3  15372