Theorem ad2ant2r 501

Description: Deduction adding two conjuncts to antecedent. (Contributed by NM, 8-Jan-2006.)

Hypothesis

Ref	Expression
ad2ant2.1	⊢ ((𝜑 ∧ 𝜓) → 𝜒)

Assertion

Ref	Expression
ad2ant2r	⊢ (((𝜑 ∧ 𝜃) ∧ (𝜓 ∧ 𝜏)) → 𝜒)

Proof of Theorem ad2ant2r

Step	Hyp	Ref	Expression
1		ad2ant2.1	. . 3 ⊢ ((𝜑 ∧ 𝜓) → 𝜒)
2	1	adantrr 471	. 2 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜏)) → 𝜒)
3	2	adantlr 469	1 ⊢ (((𝜑 ∧ 𝜃) ∧ (𝜓 ∧ 𝜏)) → 𝜒)

Syntax hints:   → wi 4   ∧ wa 103

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem is referenced by:  foco  5420  fvco4  5558  fliftfun  5764  f1imaen2g  6759  fodju0  7111  mulcomnqg  7324  mulassnqg  7325  ltdcnq  7338  lt2addnq  7345  lt2mulnq  7346  enq0ref  7374  enq0tr  7375  addcmpblnq0  7384  nqpnq0nq  7394  nqnq0m  7396  mulcomnq0  7401  addlocpr  7477  nqprl  7492  nqpru  7493  prmuloc  7507  distrlem1prl  7523  distrlem1pru  7524  ltaddpr  7538  ltexprlemopu  7544  ltexprlemdisj  7547  ltexprlemloc  7548  ltexprlemrl  7551  ltexprlemru  7553  recexprlemloc  7572  recexprlem1ssl  7574  recexprlem1ssu  7575  caucvgprprlemopu  7640  addcomsrg  7696  mulcomsrg  7698  mulasssrg  7699  distrsrg  7700  addcnsr  7775  mulcnsr  7776  addcnsrec  7783  axaddcl  7805  axaddcom  7811  addsub4  8141  muladd  8282  mullt0  8378  apreim  8501  mulge0  8517  divmuldivap  8608  divmul24ap  8612  divmuleqap  8613  recdivap  8614  divadddivap  8623  conjmulap  8625  prodgt0gt0  8746  ltmul12a  8755  lemul12b  8756  lediv2a  8790  qmulcl  9575  irrmul  9585  xrrege0  9761  ge0addcl  9917  ge0mulcl  9918  ge0xaddcl  9919  fzass4  9997  fzrev  10019  fzocatel  10134  expclzaplem  10479  expge0  10491  expge1  10492  lt2sq  10528  le2sq  10529  bernneq  10575  sq11ap  10622  sqrt11ap  10980  2clim  11242  climge0  11266  tanaddaplem  11679  opeo  11834  omeo  11835  cncongr1  12035  pcpremul  12225  pcmul  12233  ennnfonelemf1  12351  setscom  12434  opnneissb  12795  cncnpi  12868  neitx  12908  txcnmpt  12913  txrest  12916  txdis1cn  12918  ptolemy  13385  cxplt3  13480  cxple3  13481  lgslem3  13543  lgsdir2  13574  lgsne0  13579