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:  foco  5440  fvco4  5580  fliftfun  5787  f1imaen2g  6783  fodju0  7135  mulcomnqg  7357  mulassnqg  7358  ltdcnq  7371  lt2addnq  7378  lt2mulnq  7379  enq0ref  7407  enq0tr  7408  addcmpblnq0  7417  nqpnq0nq  7427  nqnq0m  7429  mulcomnq0  7434  addlocpr  7510  nqprl  7525  nqpru  7526  prmuloc  7540  distrlem1prl  7556  distrlem1pru  7557  ltaddpr  7571  ltexprlemopu  7577  ltexprlemdisj  7580  ltexprlemloc  7581  ltexprlemrl  7584  ltexprlemru  7586  recexprlemloc  7605  recexprlem1ssl  7607  recexprlem1ssu  7608  caucvgprprlemopu  7673  addcomsrg  7729  mulcomsrg  7731  mulasssrg  7732  distrsrg  7733  addcnsr  7808  mulcnsr  7809  addcnsrec  7816  axaddcl  7838  axaddcom  7844  addsub4  8174  muladd  8315  mullt0  8411  apreim  8534  mulge0  8550  divmuldivap  8642  divmul24ap  8646  divmuleqap  8647  recdivap  8648  divadddivap  8657  conjmulap  8659  prodgt0gt0  8781  ltmul12a  8790  lemul12b  8791  lediv2a  8825  qmulcl  9610  irrmul  9620  xrrege0  9796  ge0addcl  9952  ge0mulcl  9953  ge0xaddcl  9954  fzass4  10032  fzrev  10054  fzocatel  10169  expclzaplem  10514  expge0  10526  expge1  10527  lt2sq  10563  le2sq  10564  bernneq  10610  sq11ap  10657  sqrt11ap  11015  2clim  11277  climge0  11301  tanaddaplem  11714  opeo  11869  omeo  11870  cncongr1  12070  pcpremul  12260  pcmul  12268  ennnfonelemf1  12386  setscom  12469  dfgrp3mlem  12829  grplactcnv  12833  opnneissb  13226  cncnpi  13299  neitx  13339  txcnmpt  13344  txrest  13347  txdis1cn  13349  ptolemy  13816  cxplt3  13911  cxple3  13912  lgslem3  13974  lgsdir2  14005  lgsne0  14010