Theorem ad2ant2r 509

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 479	. 2 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜏)) → 𝜒)
3	2	adantlr 477	1 ⊢ (((𝜑 ∧ 𝜃) ∧ (𝜓 ∧ 𝜏)) → 𝜒)

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:  fundif  5317  foco  5508  fvco4  5650  fliftfun  5864  f1imaen2g  6884  fodju0  7248  mulcomnqg  7495  mulassnqg  7496  ltdcnq  7509  lt2addnq  7516  lt2mulnq  7517  enq0ref  7545  enq0tr  7546  addcmpblnq0  7555  nqpnq0nq  7565  nqnq0m  7567  mulcomnq0  7572  addlocpr  7648  nqprl  7663  nqpru  7664  prmuloc  7678  distrlem1prl  7694  distrlem1pru  7695  ltaddpr  7709  ltexprlemopu  7715  ltexprlemdisj  7718  ltexprlemloc  7719  ltexprlemrl  7722  ltexprlemru  7724  recexprlemloc  7743  recexprlem1ssl  7745  recexprlem1ssu  7746  caucvgprprlemopu  7811  addcomsrg  7867  mulcomsrg  7869  mulasssrg  7870  distrsrg  7871  addcnsr  7946  mulcnsr  7947  addcnsrec  7954  axaddcl  7976  axaddcom  7982  addsub4  8314  muladd  8455  mullt0  8552  apreim  8675  mulge0  8691  divmuldivap  8784  divmul24ap  8788  divmuleqap  8789  recdivap  8790  divadddivap  8799  conjmulap  8801  prodgt0gt0  8923  ltmul12a  8932  lemul12b  8933  lediv2a  8967  qmulcl  9757  irrmul  9767  xrrege0  9946  ge0addcl  10102  ge0mulcl  10103  ge0xaddcl  10104  fzass4  10183  fzrev  10205  fzocatel  10326  expclzaplem  10706  expge0  10718  expge1  10719  lt2sq  10756  le2sq  10757  bernneq  10803  sq11ap  10850  sqrt11ap  11291  2clim  11554  climge0  11578  tanaddaplem  11991  opeo  12150  omeo  12151  cncongr1  12367  pcpremul  12558  pcmul  12566  ennnfonelemf1  12731  setscom  12814  dfgrp3mlem  13372  grplactcnv  13376  issubg4m  13471  resgrpisgrp  13473  ghmpreima  13544  ghmeql  13545  conjghm  13554  rngpropd  13659  lmodprop2d  14052  opnneissb  14569  cncnpi  14642  neitx  14682  txcnmpt  14687  txrest  14690  txdis1cn  14692  ptolemy  15238  cxplt3  15334  cxple3  15335  lgslem3  15421  lgsdir2  15452  lgsne0  15457  lgsquad3  15503