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  5488  fvco4  5630  fliftfun  5840  f1imaen2g  6849  fodju0  7208  mulcomnqg  7445  mulassnqg  7446  ltdcnq  7459  lt2addnq  7466  lt2mulnq  7467  enq0ref  7495  enq0tr  7496  addcmpblnq0  7505  nqpnq0nq  7515  nqnq0m  7517  mulcomnq0  7522  addlocpr  7598  nqprl  7613  nqpru  7614  prmuloc  7628  distrlem1prl  7644  distrlem1pru  7645  ltaddpr  7659  ltexprlemopu  7665  ltexprlemdisj  7668  ltexprlemloc  7669  ltexprlemrl  7672  ltexprlemru  7674  recexprlemloc  7693  recexprlem1ssl  7695  recexprlem1ssu  7696  caucvgprprlemopu  7761  addcomsrg  7817  mulcomsrg  7819  mulasssrg  7820  distrsrg  7821  addcnsr  7896  mulcnsr  7897  addcnsrec  7904  axaddcl  7926  axaddcom  7932  addsub4  8264  muladd  8405  mullt0  8501  apreim  8624  mulge0  8640  divmuldivap  8733  divmul24ap  8737  divmuleqap  8738  recdivap  8739  divadddivap  8748  conjmulap  8750  prodgt0gt0  8872  ltmul12a  8881  lemul12b  8882  lediv2a  8916  qmulcl  9705  irrmul  9715  xrrege0  9894  ge0addcl  10050  ge0mulcl  10051  ge0xaddcl  10052  fzass4  10131  fzrev  10153  fzocatel  10269  expclzaplem  10637  expge0  10649  expge1  10650  lt2sq  10687  le2sq  10688  bernneq  10734  sq11ap  10781  sqrt11ap  11185  2clim  11447  climge0  11471  tanaddaplem  11884  opeo  12041  omeo  12042  cncongr1  12244  pcpremul  12434  pcmul  12442  ennnfonelemf1  12578  setscom  12661  dfgrp3mlem  13173  grplactcnv  13177  issubg4m  13266  resgrpisgrp  13268  ghmpreima  13339  ghmeql  13340  conjghm  13349  rngpropd  13454  lmodprop2d  13847  opnneissb  14334  cncnpi  14407  neitx  14447  txcnmpt  14452  txrest  14455  txdis1cn  14457  ptolemy  15000  cxplt3  15095  cxple3  15096  lgslem3  15159  lgsdir2  15190  lgsne0  15195  lgsquad3  15241