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  5318  foco  5509  fvco4  5651  fliftfun  5865  f1imaen2g  6885  fodju0  7249  mulcomnqg  7496  mulassnqg  7497  ltdcnq  7510  lt2addnq  7517  lt2mulnq  7518  enq0ref  7546  enq0tr  7547  addcmpblnq0  7556  nqpnq0nq  7566  nqnq0m  7568  mulcomnq0  7573  addlocpr  7649  nqprl  7664  nqpru  7665  prmuloc  7679  distrlem1prl  7695  distrlem1pru  7696  ltaddpr  7710  ltexprlemopu  7716  ltexprlemdisj  7719  ltexprlemloc  7720  ltexprlemrl  7723  ltexprlemru  7725  recexprlemloc  7744  recexprlem1ssl  7746  recexprlem1ssu  7747  caucvgprprlemopu  7812  addcomsrg  7868  mulcomsrg  7870  mulasssrg  7871  distrsrg  7872  addcnsr  7947  mulcnsr  7948  addcnsrec  7955  axaddcl  7977  axaddcom  7983  addsub4  8315  muladd  8456  mullt0  8553  apreim  8676  mulge0  8692  divmuldivap  8785  divmul24ap  8789  divmuleqap  8790  recdivap  8791  divadddivap  8800  conjmulap  8802  prodgt0gt0  8924  ltmul12a  8933  lemul12b  8934  lediv2a  8968  qmulcl  9758  irrmul  9768  xrrege0  9947  ge0addcl  10103  ge0mulcl  10104  ge0xaddcl  10105  fzass4  10184  fzrev  10206  fzocatel  10328  expclzaplem  10708  expge0  10720  expge1  10721  lt2sq  10758  le2sq  10759  bernneq  10805  sq11ap  10852  ccatw2s1p2  11097  sqrt11ap  11349  2clim  11612  climge0  11636  tanaddaplem  12049  opeo  12208  omeo  12209  cncongr1  12425  pcpremul  12616  pcmul  12624  ennnfonelemf1  12789  setscom  12872  dfgrp3mlem  13430  grplactcnv  13434  issubg4m  13529  resgrpisgrp  13531  ghmpreima  13602  ghmeql  13603  conjghm  13612  rngpropd  13717  lmodprop2d  14110  opnneissb  14627  cncnpi  14700  neitx  14740  txcnmpt  14745  txrest  14748  txdis1cn  14750  ptolemy  15296  cxplt3  15392  cxple3  15393  lgslem3  15479  lgsdir2  15510  lgsne0  15515  lgsquad3  15561