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  5371  foco  5567  fvco4  5714  fliftfun  5932  f1imaen2g  6962  fodju0  7337  mulcomnqg  7593  mulassnqg  7594  ltdcnq  7607  lt2addnq  7614  lt2mulnq  7615  enq0ref  7643  enq0tr  7644  addcmpblnq0  7653  nqpnq0nq  7663  nqnq0m  7665  mulcomnq0  7670  addlocpr  7746  nqprl  7761  nqpru  7762  prmuloc  7776  distrlem1prl  7792  distrlem1pru  7793  ltaddpr  7807  ltexprlemopu  7813  ltexprlemdisj  7816  ltexprlemloc  7817  ltexprlemrl  7820  ltexprlemru  7822  recexprlemloc  7841  recexprlem1ssl  7843  recexprlem1ssu  7844  caucvgprprlemopu  7909  addcomsrg  7965  mulcomsrg  7967  mulasssrg  7968  distrsrg  7969  addcnsr  8044  mulcnsr  8045  addcnsrec  8052  axaddcl  8074  axaddcom  8080  addsub4  8412  muladd  8553  mullt0  8650  apreim  8773  mulge0  8789  divmuldivap  8882  divmul24ap  8886  divmuleqap  8887  recdivap  8888  divadddivap  8897  conjmulap  8899  prodgt0gt0  9021  ltmul12a  9030  lemul12b  9031  lediv2a  9065  qmulcl  9861  irrmul  9871  xrrege0  10050  ge0addcl  10206  ge0mulcl  10207  ge0xaddcl  10208  fzass4  10287  fzrev  10309  fzocatel  10434  expclzaplem  10815  expge0  10827  expge1  10828  lt2sq  10865  le2sq  10866  bernneq  10912  sq11ap  10959  ccatw2s1p1g  11212  ccatw2s1p2  11213  swrdccatin2  11300  sqrt11ap  11589  2clim  11852  climge0  11876  tanaddaplem  12289  opeo  12448  omeo  12449  cncongr1  12665  pcpremul  12856  pcmul  12864  ennnfonelemf1  13029  setscom  13112  dfgrp3mlem  13671  grplactcnv  13675  issubg4m  13770  resgrpisgrp  13772  ghmpreima  13843  ghmeql  13844  conjghm  13853  rngpropd  13958  lmodprop2d  14352  opnneissb  14869  cncnpi  14942  neitx  14982  txcnmpt  14987  txrest  14990  txdis1cn  14992  ptolemy  15538  cxplt3  15634  cxple3  15635  lgslem3  15721  lgsdir2  15752  lgsne0  15757  lgsquad3  15803  umgr2edg  16046  umgrvad2edg  16050  wlkeq  16151  clwwlkccatlem  16195