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  5365  foco  5561  fvco4  5708  fliftfun  5926  f1imaen2g  6953  fodju0  7325  mulcomnqg  7581  mulassnqg  7582  ltdcnq  7595  lt2addnq  7602  lt2mulnq  7603  enq0ref  7631  enq0tr  7632  addcmpblnq0  7641  nqpnq0nq  7651  nqnq0m  7653  mulcomnq0  7658  addlocpr  7734  nqprl  7749  nqpru  7750  prmuloc  7764  distrlem1prl  7780  distrlem1pru  7781  ltaddpr  7795  ltexprlemopu  7801  ltexprlemdisj  7804  ltexprlemloc  7805  ltexprlemrl  7808  ltexprlemru  7810  recexprlemloc  7829  recexprlem1ssl  7831  recexprlem1ssu  7832  caucvgprprlemopu  7897  addcomsrg  7953  mulcomsrg  7955  mulasssrg  7956  distrsrg  7957  addcnsr  8032  mulcnsr  8033  addcnsrec  8040  axaddcl  8062  axaddcom  8068  addsub4  8400  muladd  8541  mullt0  8638  apreim  8761  mulge0  8777  divmuldivap  8870  divmul24ap  8874  divmuleqap  8875  recdivap  8876  divadddivap  8885  conjmulap  8887  prodgt0gt0  9009  ltmul12a  9018  lemul12b  9019  lediv2a  9053  qmulcl  9844  irrmul  9854  xrrege0  10033  ge0addcl  10189  ge0mulcl  10190  ge0xaddcl  10191  fzass4  10270  fzrev  10292  fzocatel  10417  expclzaplem  10797  expge0  10809  expge1  10810  lt2sq  10847  le2sq  10848  bernneq  10894  sq11ap  10941  ccatw2s1p2  11191  swrdccatin2  11276  sqrt11ap  11564  2clim  11827  climge0  11851  tanaddaplem  12264  opeo  12423  omeo  12424  cncongr1  12640  pcpremul  12831  pcmul  12839  ennnfonelemf1  13004  setscom  13087  dfgrp3mlem  13646  grplactcnv  13650  issubg4m  13745  resgrpisgrp  13747  ghmpreima  13818  ghmeql  13819  conjghm  13828  rngpropd  13933  lmodprop2d  14327  opnneissb  14844  cncnpi  14917  neitx  14957  txcnmpt  14962  txrest  14965  txdis1cn  14967  ptolemy  15513  cxplt3  15609  cxple3  15610  lgslem3  15696  lgsdir2  15727  lgsne0  15732  lgsquad3  15778  umgr2edg  16020  umgrvad2edg  16024  wlkeq  16095  clwwlkccatlem  16137