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  5487  fvco4  5629  fliftfun  5839  f1imaen2g  6847  fodju0  7206  mulcomnqg  7443  mulassnqg  7444  ltdcnq  7457  lt2addnq  7464  lt2mulnq  7465  enq0ref  7493  enq0tr  7494  addcmpblnq0  7503  nqpnq0nq  7513  nqnq0m  7515  mulcomnq0  7520  addlocpr  7596  nqprl  7611  nqpru  7612  prmuloc  7626  distrlem1prl  7642  distrlem1pru  7643  ltaddpr  7657  ltexprlemopu  7663  ltexprlemdisj  7666  ltexprlemloc  7667  ltexprlemrl  7670  ltexprlemru  7672  recexprlemloc  7691  recexprlem1ssl  7693  recexprlem1ssu  7694  caucvgprprlemopu  7759  addcomsrg  7815  mulcomsrg  7817  mulasssrg  7818  distrsrg  7819  addcnsr  7894  mulcnsr  7895  addcnsrec  7902  axaddcl  7924  axaddcom  7930  addsub4  8262  muladd  8403  mullt0  8499  apreim  8622  mulge0  8638  divmuldivap  8731  divmul24ap  8735  divmuleqap  8736  recdivap  8737  divadddivap  8746  conjmulap  8748  prodgt0gt0  8870  ltmul12a  8879  lemul12b  8880  lediv2a  8914  qmulcl  9702  irrmul  9712  xrrege0  9891  ge0addcl  10047  ge0mulcl  10048  ge0xaddcl  10049  fzass4  10128  fzrev  10150  fzocatel  10266  expclzaplem  10634  expge0  10646  expge1  10647  lt2sq  10684  le2sq  10685  bernneq  10731  sq11ap  10778  sqrt11ap  11182  2clim  11444  climge0  11468  tanaddaplem  11881  opeo  12038  omeo  12039  cncongr1  12241  pcpremul  12431  pcmul  12439  ennnfonelemf1  12575  setscom  12658  dfgrp3mlem  13170  grplactcnv  13174  issubg4m  13263  resgrpisgrp  13265  ghmpreima  13336  ghmeql  13337  conjghm  13346  rngpropd  13451  lmodprop2d  13844  opnneissb  14323  cncnpi  14396  neitx  14436  txcnmpt  14441  txrest  14444  txdis1cn  14446  ptolemy  14959  cxplt3  15054  cxple3  15055  lgslem3  15118  lgsdir2  15149  lgsne0  15154