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  9071  ccatswrd  14576  plttr  18246  pltletr  18247  latjlej1  18359  latjlej2  18360  latnlej  18362  latnlej2  18365  latmlem2  18376  latledi  18383  latjass  18389  latj32  18391  latj13  18392  ipopos  18442  tsrlemax  18492  imasmnd2  18682  grpsubsub  18942  grpnnncan2  18950  imasgrp2  18968  mulgnn0ass  19023  mulgsubdir  19027  cmn32  19712  ablsubadd  19721  imasrng  20095  imasring  20248  isdomn4  20631  zntoslem  21493  xmettri3  24268  mettri3  24269  xmetrtri  24270  xmetrtri2  24271  metrtri  24272  cphdivcl  25109  cphassr  25139  relogbmulexp  26715  grpodivdiv  30520  grpomuldivass  30521  ablo32  30529  ablodivdiv4  30534  ablodiv32  30535  nvmdi  30628  dipdi  30823  dipassr  30826  dipsubdir  30828  dipsubdi  30829  dvrcan5  33203  cgr3tr4  36094  cgr3rflx  36096  endofsegid  36127  seglemin  36155  broutsideof2  36164  rngosubdi  37993  rngosubdir  37994  isdrngo2  38006  crngm23  38050  dmncan2  38125  latmassOLD  39276  latm32  39278  cvrnbtwn4  39326  cvrcmp2  39331  ltcvrntr  39471  atcvrj0  39475  3dim3  39516  paddasslem17  39883  paddass  39885  lautlt  40138  lautcvr  40139  lautj  40140  lautm  40141  erngdvlem3  41037  dvalveclem  41072  mendlmod  43230