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  9124  ccatswrd  14633  plttr  18301  pltletr  18302  latjlej1  18412  latjlej2  18413  latnlej  18415  latnlej2  18418  latmlem2  18429  latledi  18436  latjass  18442  latj32  18444  latj13  18445  ipopos  18495  tsrlemax  18545  imasmnd2  18701  grpsubsub  18961  grpnnncan2  18969  imasgrp2  18987  mulgnn0ass  19042  mulgsubdir  19046  cmn32  19730  ablsubadd  19739  imasrng  20086  imasring  20239  isdomn4  20625  zntoslem  21466  xmettri3  24241  mettri3  24242  xmetrtri  24243  xmetrtri2  24244  metrtri  24245  cphdivcl  25082  cphassr  25112  relogbmulexp  26688  grpodivdiv  30469  grpomuldivass  30470  ablo32  30478  ablodivdiv4  30483  ablodiv32  30484  nvmdi  30577  dipdi  30772  dipassr  30775  dipsubdir  30777  dipsubdi  30778  dvrcan5  33187  cgr3tr4  36040  cgr3rflx  36042  endofsegid  36073  seglemin  36101  broutsideof2  36110  rngosubdi  37939  rngosubdir  37940  isdrngo2  37952  crngm23  37996  dmncan2  38071  latmassOLD  39222  latm32  39224  cvrnbtwn4  39272  cvrcmp2  39277  ltcvrntr  39418  atcvrj0  39422  3dim3  39463  paddasslem17  39830  paddass  39832  lautlt  40085  lautcvr  40086  lautj  40087  lautm  40088  erngdvlem3  40984  dvalveclem  41019  mendlmod  43178