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  10444  expclzaplem  10825  expge0  10837  expge1  10838  lt2sq  10875  le2sq  10876  bernneq  10922  sq11ap  10969  ccatw2s1p1g  11222  ccatw2s1p2  11223  swrdccatin2  11310  sqrt11ap  11599  2clim  11862  climge0  11886  tanaddaplem  12300  opeo  12459  omeo  12460  cncongr1  12676  pcpremul  12867  pcmul  12875  ennnfonelemf1  13040  setscom  13123  dfgrp3mlem  13682  grplactcnv  13686  issubg4m  13781  resgrpisgrp  13783  ghmpreima  13854  ghmeql  13855  conjghm  13864  rngpropd  13970  lmodprop2d  14364  opnneissb  14881  cncnpi  14954  neitx  14994  txcnmpt  14999  txrest  15002  txdis1cn  15004  ptolemy  15550  cxplt3  15646  cxple3  15647  lgslem3  15733  lgsdir2  15764  lgsne0  15769  lgsquad3  15815  umgr2edg  16060  umgrvad2edg  16064  wlkeq  16207  clwwlkccatlem  16253