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  5332  foco  5526  fvco4  5669  fliftfun  5883  f1imaen2g  6903  fodju0  7270  mulcomnqg  7526  mulassnqg  7527  ltdcnq  7540  lt2addnq  7547  lt2mulnq  7548  enq0ref  7576  enq0tr  7577  addcmpblnq0  7586  nqpnq0nq  7596  nqnq0m  7598  mulcomnq0  7603  addlocpr  7679  nqprl  7694  nqpru  7695  prmuloc  7709  distrlem1prl  7725  distrlem1pru  7726  ltaddpr  7740  ltexprlemopu  7746  ltexprlemdisj  7749  ltexprlemloc  7750  ltexprlemrl  7753  ltexprlemru  7755  recexprlemloc  7774  recexprlem1ssl  7776  recexprlem1ssu  7777  caucvgprprlemopu  7842  addcomsrg  7898  mulcomsrg  7900  mulasssrg  7901  distrsrg  7902  addcnsr  7977  mulcnsr  7978  addcnsrec  7985  axaddcl  8007  axaddcom  8013  addsub4  8345  muladd  8486  mullt0  8583  apreim  8706  mulge0  8722  divmuldivap  8815  divmul24ap  8819  divmuleqap  8820  recdivap  8821  divadddivap  8830  conjmulap  8832  prodgt0gt0  8954  ltmul12a  8963  lemul12b  8964  lediv2a  8998  qmulcl  9788  irrmul  9798  xrrege0  9977  ge0addcl  10133  ge0mulcl  10134  ge0xaddcl  10135  fzass4  10214  fzrev  10236  fzocatel  10360  expclzaplem  10740  expge0  10752  expge1  10753  lt2sq  10790  le2sq  10791  bernneq  10837  sq11ap  10884  ccatw2s1p2  11130  sqrt11ap  11434  2clim  11697  climge0  11721  tanaddaplem  12134  opeo  12293  omeo  12294  cncongr1  12510  pcpremul  12701  pcmul  12709  ennnfonelemf1  12874  setscom  12957  dfgrp3mlem  13515  grplactcnv  13519  issubg4m  13614  resgrpisgrp  13616  ghmpreima  13687  ghmeql  13688  conjghm  13697  rngpropd  13802  lmodprop2d  14195  opnneissb  14712  cncnpi  14785  neitx  14825  txcnmpt  14830  txrest  14833  txdis1cn  14835  ptolemy  15381  cxplt3  15477  cxple3  15478  lgslem3  15564  lgsdir2  15595  lgsne0  15600  lgsquad3  15646