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  7084  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  10053  irrmul  10064  xrrege0  10244  ge0addcl  10400  ge0mulcl  10401  ge0xaddcl  10402  fzass4  10485  fzrev  10508  fzocatel  10634  expclzaplem  11021  expge0  11033  expge1  11034  lt2sq  11071  le2sq  11072  bernneq  11119  sq11ap  11166  ccatw2s1p1g  11435  ccatw2s1p2  11436  swrdccatin2  11523  sqrt11ap  11826  2clim  12092  climge0  12116  tanaddaplem  12530  opeo  12689  omeo  12690  cncongr1  12906  pcpremul  13101  pcmul  13109  ennnfonelemf1  13367  setscom  13450  dfgrp3mlem  13962  grplactcnv  13966  issubg4m  14055  resgrpisgrp  14057  ghmpreima  14128  ghmeql  14129  conjghm  14138  rngpropd  14361  lmodprop2d  14794  opnneissb  15381  cncnpi  15454  neitx  15494  txcnmpt  15499  txrest  15502  txdis1cn  15504  ptolemy  16051  cxplt3  16155  cxple3  16156  lgslem3  16326  lgsdir2  16357  lgsne0  16362  lgsquad3  16408  umgr2edg  16653  umgrvad2edg  16657  wlkeq  16800  clwwlkccatlem  16846