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  5405  foco  5606  fvco4  5754  fliftfun  5975  f1imaen2g  7046  fodju0  7451  mulcomnqg  7714  mulassnqg  7715  ltdcnq  7728  lt2addnq  7735  lt2mulnq  7736  enq0ref  7764  enq0tr  7765  addcmpblnq0  7774  nqpnq0nq  7784  nqnq0m  7786  mulcomnq0  7791  addlocpr  7867  nqprl  7882  nqpru  7883  prmuloc  7897  distrlem1prl  7913  distrlem1pru  7914  ltaddpr  7928  ltexprlemopu  7934  ltexprlemdisj  7937  ltexprlemloc  7938  ltexprlemrl  7941  ltexprlemru  7943  recexprlemloc  7962  recexprlem1ssl  7964  recexprlem1ssu  7965  caucvgprprlemopu  8030  addcomsrg  8086  mulcomsrg  8088  mulasssrg  8089  distrsrg  8090  addcnsr  8165  mulcnsr  8166  addcnsrec  8173  axaddcl  8195  axaddcom  8201  addsub4  8532  muladd  8674  mullt0  8771  apreim  8894  mulge0  8910  divmuldivap  9003  divmul24ap  9007  divmuleqap  9008  recdivap  9009  divadddivap  9018  conjmulap  9020  prodgt0gt0  9142  ltmul12a  9151  lemul12b  9152  lediv2a  9186  qmulcl  9987  irrmul  9997  xrrege0  10177  ge0addcl  10333  ge0mulcl  10334  ge0xaddcl  10335  fzass4  10417  fzrev  10440  fzocatel  10566  expclzaplem  10949  expge0  10961  expge1  10962  lt2sq  10999  le2sq  11000  bernneq  11047  sq11ap  11094  ccatw2s1p1g  11358  ccatw2s1p2  11359  swrdccatin2  11446  sqrt11ap  11748  2clim  12011  climge0  12035  tanaddaplem  12449  opeo  12608  omeo  12609  cncongr1  12825  pcpremul  13016  pcmul  13024  ennnfonelemf1  13253  setscom  13336  dfgrp3mlem  13853  grplactcnv  13857  issubg4m  13946  resgrpisgrp  13948  ghmpreima  14019  ghmeql  14020  conjghm  14029  rngpropd  14194  lmodprop2d  14622  opnneissb  15146  cncnpi  15219  neitx  15259  txcnmpt  15264  txrest  15267  txdis1cn  15269  ptolemy  15815  cxplt3  15911  cxple3  15912  lgslem3  16001  lgsdir2  16032  lgsne0  16037  lgsquad3  16083  umgr2edg  16328  umgrvad2edg  16332  wlkeq  16475  clwwlkccatlem  16521