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  5374  foco  5570  fvco4  5718  fliftfun  5937  f1imaen2g  6967  fodju0  7346  mulcomnqg  7603  mulassnqg  7604  ltdcnq  7617  lt2addnq  7624  lt2mulnq  7625  enq0ref  7653  enq0tr  7654  addcmpblnq0  7663  nqpnq0nq  7673  nqnq0m  7675  mulcomnq0  7680  addlocpr  7756  nqprl  7771  nqpru  7772  prmuloc  7786  distrlem1prl  7802  distrlem1pru  7803  ltaddpr  7817  ltexprlemopu  7823  ltexprlemdisj  7826  ltexprlemloc  7827  ltexprlemrl  7830  ltexprlemru  7832  recexprlemloc  7851  recexprlem1ssl  7853  recexprlem1ssu  7854  caucvgprprlemopu  7919  addcomsrg  7975  mulcomsrg  7977  mulasssrg  7978  distrsrg  7979  addcnsr  8054  mulcnsr  8055  addcnsrec  8062  axaddcl  8084  axaddcom  8090  addsub4  8422  muladd  8563  mullt0  8660  apreim  8783  mulge0  8799  divmuldivap  8892  divmul24ap  8896  divmuleqap  8897  recdivap  8898  divadddivap  8907  conjmulap  8909  prodgt0gt0  9031  ltmul12a  9040  lemul12b  9041  lediv2a  9075  qmulcl  9871  irrmul  9881  xrrege0  10060  ge0addcl  10216  ge0mulcl  10217  ge0xaddcl  10218  fzass4  10297  fzrev  10319  fzocatel  10445  expclzaplem  10826  expge0  10838  expge1  10839  lt2sq  10876  le2sq  10877  bernneq  10923  sq11ap  10970  ccatw2s1p1g  11226  ccatw2s1p2  11227  swrdccatin2  11314  sqrt11ap  11603  2clim  11866  climge0  11890  tanaddaplem  12304  opeo  12463  omeo  12464  cncongr1  12680  pcpremul  12871  pcmul  12879  ennnfonelemf1  13044  setscom  13127  dfgrp3mlem  13686  grplactcnv  13690  issubg4m  13785  resgrpisgrp  13787  ghmpreima  13858  ghmeql  13859  conjghm  13868  rngpropd  13974  lmodprop2d  14368  opnneissb  14885  cncnpi  14958  neitx  14998  txcnmpt  15003  txrest  15006  txdis1cn  15008  ptolemy  15554  cxplt3  15650  cxple3  15651  lgslem3  15737  lgsdir2  15768  lgsne0  15773  lgsquad3  15819  umgr2edg  16064  umgrvad2edg  16068  wlkeq  16211  clwwlkccatlem  16257