Theorem 3adant3r1 1183

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 1120	. 2 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)
3	2	3adantr1 1170	1 ⊢ ((𝜑 ∧ (𝜏 ∧ 𝜓 ∧ 𝜒)) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1086

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 207  df-an 396  df-3an 1088

This theorem is referenced by:  dif1en  9101  ccatswrd  14609  plttr  18281  pltletr  18282  latjlej1  18394  latjlej2  18395  latnlej  18397  latnlej2  18400  latmlem2  18411  latledi  18418  latjass  18424  latj32  18426  latj13  18427  ipopos  18477  tsrlemax  18527  imasmnd2  18683  grpsubsub  18943  grpnnncan2  18951  imasgrp2  18969  mulgnn0ass  19024  mulgsubdir  19028  cmn32  19714  ablsubadd  19723  imasrng  20097  imasring  20250  isdomn4  20636  zntoslem  21498  xmettri3  24274  mettri3  24275  xmetrtri  24276  xmetrtri2  24277  metrtri  24278  cphdivcl  25115  cphassr  25145  relogbmulexp  26721  grpodivdiv  30519  grpomuldivass  30520  ablo32  30528  ablodivdiv4  30533  ablodiv32  30534  nvmdi  30627  dipdi  30822  dipassr  30825  dipsubdir  30827  dipsubdi  30828  dvrcan5  33203  cgr3tr4  36033  cgr3rflx  36035  endofsegid  36066  seglemin  36094  broutsideof2  36103  rngosubdi  37932  rngosubdir  37933  isdrngo2  37945  crngm23  37989  dmncan2  38064  latmassOLD  39215  latm32  39217  cvrnbtwn4  39265  cvrcmp2  39270  ltcvrntr  39411  atcvrj0  39415  3dim3  39456  paddasslem17  39823  paddass  39825  lautlt  40078  lautcvr  40079  lautj  40080  lautm  40081  erngdvlem3  40977  dvalveclem  41012  mendlmod  43171