Theorem 3adant3r1 1199

Description: Deduction adding a conjunct to antecedent. (Contributed by NM, 16-Feb-2008.)

Hypothesis

Ref	Expression
ad4ant3.1	⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

Assertion

Ref	Expression
3adant3r1	⊢ ((𝜑 ∧ (𝜏 ∧ 𝜓 ∧ 𝜒)) → 𝜃)

Proof of Theorem 3adant3r1

Step	Hyp	Ref	Expression
1		ad4ant3.1	. . 3 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)
2	1	3expb 1136	. 2 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)
3	2	3adantr1 1186	1 ⊢ ((𝜑 ∧ (𝜏 ∧ 𝜓 ∧ 𝜒)) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1101

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 210  df-an 401  df-3an 1103

This theorem is referenced by:  dif1en  9145  ccatswrd  14705  plttr  18395  pltletr  18396  latjlej1  18508  latjlej2  18509  latnlej  18511  latnlej2  18514  latmlem2  18525  latledi  18532  latjass  18538  latj32  18540  latj13  18541  ipopos  18591  tsrlemax  18641  imasmnd2  18831  grpsubsub  19094  grpnnncan2  19102  imasgrp2  19120  mulgnn0ass  19175  mulgsubdir  19179  cmn32  19869  ablsubadd  19878  imasrng  20254  imasring  20411  isdomn4  20799  zntoslem  21674  xmettri3  24478  mettri3  24479  xmetrtri  24480  xmetrtri2  24481  metrtri  24482  cphdivcl  25309  cphassr  25339  relogbmulexp  26908  grpodivdiv  30832  grpomuldivass  30833  ablo32  30841  ablodivdiv4  30846  ablodiv32  30847  nvmdi  30940  dipdi  31135  dipassr  31138  dipsubdir  31140  dipsubdi  31141  dvrcan5  33495  cgr3tr4  36442  cgr3rflx  36444  endofsegid  36475  seglemin  36503  broutsideof2  36512  rngosubdi  38483  rngosubdir  38484  isdrngo2  38496  crngm23  38540  dmncan2  38615  latmassOLD  39892  latm32  39894  cvrnbtwn4  39942  cvrcmp2  39947  ltcvrntr  40087  atcvrj0  40091  3dim3  40132  paddasslem17  40499  paddass  40501  lautlt  40754  lautcvr  40755  lautj  40756  lautm  40757  erngdvlem3  41653  dvalveclem  41688  mendlmod  43807