Theorem 3adant3r1 1182

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 1169	1 ⊢ ((𝜑 ∧ (𝜏 ∧ 𝜓 ∧ 𝜒)) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 396   ∧ w3a 1087

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 206  df-an 397  df-3an 1089

This theorem is referenced by:  dif1en  9162  ccatswrd  14622  plttr  18299  pltletr  18300  latjlej1  18410  latjlej2  18411  latnlej  18413  latnlej2  18416  latmlem2  18427  latledi  18434  latjass  18440  latj32  18442  latj13  18443  ipopos  18493  tsrlemax  18543  imasmnd2  18696  grpsubsub  18948  grpnnncan2  18956  imasgrp2  18974  mulgnn0ass  19026  mulgsubdir  19030  cmn32  19709  ablsubadd  19718  imasrng  20071  imasring  20218  isdomn4  21118  zntoslem  21331  xmettri3  24079  mettri3  24080  xmetrtri  24081  xmetrtri2  24082  metrtri  24083  cphdivcl  24923  cphassr  24953  relogbmulexp  26507  grpodivdiv  30048  grpomuldivass  30049  ablo32  30057  ablodivdiv4  30062  ablodiv32  30063  nvmdi  30156  dipdi  30351  dipassr  30354  dipsubdir  30356  dipsubdi  30357  dvrcan5  32643  cgr3tr4  35316  cgr3rflx  35318  endofsegid  35349  seglemin  35377  broutsideof2  35386  rngosubdi  37116  rngosubdir  37117  isdrngo2  37129  crngm23  37173  dmncan2  37248  latmassOLD  38402  latm32  38404  cvrnbtwn4  38452  cvrcmp2  38457  ltcvrntr  38598  atcvrj0  38602  3dim3  38643  paddasslem17  39010  paddass  39012  lautlt  39265  lautcvr  39266  lautj  39267  lautm  39268  erngdvlem3  40164  dvalveclem  40199  mendlmod  42237