Theorem ad2ant2r 513

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 483	. 2 |- ( ( ph /\ ( ps /\ ta ) ) -> ch )
3	2	adantlr 481	1 |- ( ( ( ph /\ th ) /\ ( ps /\ ta ) ) -> ch )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem is used by:  fundif  5425  foco  5626  fvco4  5777  fliftfun  6002  f1imaen2g  7080  fodju0  7488  mulcomnqg  7751  mulassnqg  7752  ltdcnq  7765  lt2addnq  7772  lt2mulnq  7773  enq0ref  7801  enq0tr  7802  addcmpblnq0  7811  nqpnq0nq  7821  nqnq0m  7823  mulcomnq0  7828  addlocpr  7904  nqprl  7919  nqpru  7920  prmuloc  7934  distrlem1prl  7950  distrlem1pru  7951  ltaddpr  7965  ltexprlemopu  7971  ltexprlemdisj  7974  ltexprlemloc  7975  ltexprlemrl  7978  ltexprlemru  7980  recexprlemloc  7999  recexprlem1ssl  8001  recexprlem1ssu  8002  caucvgprprlemopu  8067  addcomsrg  8123  mulcomsrg  8125  mulasssrg  8126  distrsrg  8127  addcnsr  8202  mulcnsr  8203  addcnsrec  8210  axaddcl  8232  axaddcom  8238  addsub4  8571  muladd  8713  mullt0  8810  apreim  8934  mulge0  8950  divmuldivap  9045  divmul24ap  9049  divmuleqap  9050  recdivap  9051  divadddivap  9060  conjmulap  9062  prodgt0gt0  9184  ltmul12a  9193  lemul12b  9194  lediv2a  9228  qmulcl  10047  irrmul  10058  xrrege0  10238  ge0addcl  10394  ge0mulcl  10395  ge0xaddcl  10396  fzass4  10479  fzrev  10502  fzocatel  10628  expclzaplem  11015  expge0  11027  expge1  11028  lt2sq  11065  le2sq  11066  bernneq  11113  sq11ap  11160  ccatw2s1p1g  11429  ccatw2s1p2  11430  swrdccatin2  11517  sqrt11ap  11820  2clim  12086  climge0  12110  tanaddaplem  12524  opeo  12683  omeo  12684  cncongr1  12900  pcpremul  13095  pcmul  13103  ennnfonelemf1  13361  setscom  13444  dfgrp3mlem  13956  grplactcnv  13960  issubg4m  14049  resgrpisgrp  14051  ghmpreima  14122  ghmeql  14123  conjghm  14132  rngpropd  14338  lmodprop2d  14769  opnneissb  15347  cncnpi  15420  neitx  15460  txcnmpt  15465  txrest  15468  txdis1cn  15470  ptolemy  16017  cxplt3  16117  cxple3  16118  lgslem3  16287  lgsdir2  16318  lgsne0  16323  lgsquad3  16369  umgr2edg  16614  umgrvad2edg  16618  wlkeq  16761  clwwlkccatlem  16807