Theorem 3adant3r1 1201

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  dif1en  9170  ccatswrd  14811  plttr  18507  pltletr  18508  latjlej1  18620  latjlej2  18621  latnlej  18623  latnlej2  18626  latmlem2  18637  latledi  18644  latjass  18650  latj32  18652  latj13  18653  ipopos  18703  tsrlemax  18753  imasmnd2  18961  grpsubsub  19232  grpnnncan2  19240  imasgrp2  19258  mulgnn0ass  19313  mulgsubdir  19317  cmn32  20007  ablsubadd  20016  imasrng  20392  imasring  20553  isdomn4  20960  zntoslem  21855  xmettri3  24665  mettri3  24666  xmetrtri  24667  xmetrtri2  24668  metrtri  24669  cphdivcl  25496  cphassr  25526  relogbmulexp  27099  grpodivdiv  31135  grpomuldivass  31136  ablo32  31144  ablodivdiv4  31149  ablodiv32  31150  nvmdi  31243  dipdi  31438  dipassr  31441  dipsubdir  31443  dipsubdi  31444  dvrcan5  33789  cgr3tr4  36797  cgr3rflx  36799  endofsegid  36830  seglemin  36858  broutsideof2  36867  rngosubdi  38859  rngosubdir  38860  isdrngo2  38872  crngm23  38916  dmncan2  38991  latmassOLD  40266  latm32  40268  cvrnbtwn4  40316  cvrcmp2  40321  ltcvrntr  40461  atcvrj0  40465  3dim3  40506  paddasslem17  40873  paddass  40875  lautlt  41128  lautcvr  41129  lautj  41130  lautm  41131  erngdvlem3  42027  dvalveclem  42062  mendlmod  44175  idomcanr  49414