Theorem 3adant3r1 1180

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

Syntax hints:   → wi 4   ∧ wa 394   ∧ w3a 1085

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 395  df-3an 1087

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  24930  cphassr  24960  relogbmulexp  26519  grpodivdiv  30060  grpomuldivass  30061  ablo32  30069  ablodivdiv4  30074  ablodiv32  30075  nvmdi  30168  dipdi  30363  dipassr  30366  dipsubdir  30368  dipsubdi  30369  dvrcan5  32655  cgr3tr4  35328  cgr3rflx  35330  endofsegid  35361  seglemin  35389  broutsideof2  35398  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