Theorem ad2ant2r 513

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 483	. 2 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜏)) → 𝜒)
3	2	adantlr 481	1 ⊢ (((𝜑 ∧ 𝜃) ∧ (𝜓 ∧ 𝜏)) → 𝜒)

This proof depends on syntax axioms:   → wi 4   ∧ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem is used by:  fundif  5428  foco  5629  fvco4  5780  fliftfun  6005  f1imaen2g  7086  fodju0  7493  mulcomnqg  7756  mulassnqg  7757  ltdcnq  7770  lt2addnq  7777  lt2mulnq  7778  enq0ref  7806  enq0tr  7807  addcmpblnq0  7816  nqpnq0nq  7826  nqnq0m  7828  mulcomnq0  7833  addlocpr  7909  nqprl  7924  nqpru  7925  prmuloc  7939  distrlem1prl  7955  distrlem1pru  7956  ltaddpr  7970  ltexprlemopu  7976  ltexprlemdisj  7979  ltexprlemloc  7980  ltexprlemrl  7983  ltexprlemru  7985  recexprlemloc  8004  recexprlem1ssl  8006  recexprlem1ssu  8007  caucvgprprlemopu  8072  addcomsrg  8128  mulcomsrg  8130  mulasssrg  8131  distrsrg  8132  addcnsr  8207  mulcnsr  8208  addcnsrec  8215  axaddcl  8237  axaddcom  8243  addsub4  8576  muladd  8718  mullt0  8815  apreim  8939  mulge0  8955  divmuldivap  9050  divmul24ap  9054  divmuleqap  9055  recdivap  9056  divadddivap  9065  conjmulap  9067  prodgt0gt0  9189  ltmul12a  9198  lemul12b  9199  lediv2a  9233  qmulcl  10052  irrmul  10063  xrrege0  10243  ge0addcl  10399  ge0mulcl  10400  ge0xaddcl  10401  fzass4  10484  fzrev  10507  fzocatel  10633  expclzaplem  11020  expge0  11032  expge1  11033  lt2sq  11070  le2sq  11071  bernneq  11118  sq11ap  11165  ccatw2s1p1g  11434  ccatw2s1p2  11435  swrdccatin2  11522  sqrt11ap  11825  2clim  12091  climge0  12115  tanaddaplem  12529  opeo  12688  omeo  12689  cncongr1  12905  pcpremul  13100  pcmul  13108  ennnfonelemf1  13366  setscom  13449  dfgrp3mlem  13961  grplactcnv  13965  issubg4m  14054  resgrpisgrp  14056  ghmpreima  14127  ghmeql  14128  conjghm  14137  rngpropd  14360  lmodprop2d  14793  mvrclfi  15226  opnneissb  15398  cncnpi  15471  neitx  15511  txcnmpt  15516  txrest  15519  txdis1cn  15521  ptolemy  16068  cxplt3  16172  cxple3  16173  lgslem3  16343  lgsdir2  16374  lgsne0  16379  lgsquad3  16425  umgr2edg  16670  umgrvad2edg  16674  wlkeq  16817  clwwlkccatlem  16863