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  5381  foco  5579  fvco4  5727  fliftfun  5947  f1imaen2g  7010  fodju0  7389  mulcomnqg  7646  mulassnqg  7647  ltdcnq  7660  lt2addnq  7667  lt2mulnq  7668  enq0ref  7696  enq0tr  7697  addcmpblnq0  7706  nqpnq0nq  7716  nqnq0m  7718  mulcomnq0  7723  addlocpr  7799  nqprl  7814  nqpru  7815  prmuloc  7829  distrlem1prl  7845  distrlem1pru  7846  ltaddpr  7860  ltexprlemopu  7866  ltexprlemdisj  7869  ltexprlemloc  7870  ltexprlemrl  7873  ltexprlemru  7875  recexprlemloc  7894  recexprlem1ssl  7896  recexprlem1ssu  7897  caucvgprprlemopu  7962  addcomsrg  8018  mulcomsrg  8020  mulasssrg  8021  distrsrg  8022  addcnsr  8097  mulcnsr  8098  addcnsrec  8105  axaddcl  8127  axaddcom  8133  addsub4  8464  muladd  8605  mullt0  8702  apreim  8825  mulge0  8841  divmuldivap  8934  divmul24ap  8938  divmuleqap  8939  recdivap  8940  divadddivap  8949  conjmulap  8951  prodgt0gt0  9073  ltmul12a  9082  lemul12b  9083  lediv2a  9117  qmulcl  9915  irrmul  9925  xrrege0  10104  ge0addcl  10260  ge0mulcl  10261  ge0xaddcl  10262  fzass4  10342  fzrev  10364  fzocatel  10490  expclzaplem  10871  expge0  10883  expge1  10884  lt2sq  10921  le2sq  10922  bernneq  10968  sq11ap  11015  ccatw2s1p1g  11271  ccatw2s1p2  11272  swrdccatin2  11359  sqrt11ap  11661  2clim  11924  climge0  11948  tanaddaplem  12362  opeo  12521  omeo  12522  cncongr1  12738  pcpremul  12929  pcmul  12937  ennnfonelemf1  13102  setscom  13185  dfgrp3mlem  13744  grplactcnv  13748  issubg4m  13843  resgrpisgrp  13845  ghmpreima  13916  ghmeql  13917  conjghm  13926  rngpropd  14032  lmodprop2d  14427  opnneissb  14949  cncnpi  15022  neitx  15062  txcnmpt  15067  txrest  15070  txdis1cn  15072  ptolemy  15618  cxplt3  15714  cxple3  15715  lgslem3  15804  lgsdir2  15835  lgsne0  15840  lgsquad3  15886  umgr2edg  16131  umgrvad2edg  16135  wlkeq  16278  clwwlkccatlem  16324