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  9185  ccatswrd  14826  plttr  18523  pltletr  18524  latjlej1  18636  latjlej2  18637  latnlej  18639  latnlej2  18642  latmlem2  18653  latledi  18660  latjass  18666  latj32  18668  latj13  18669  ipopos  18719  tsrlemax  18769  imasmnd2  18977  grpsubsub  19248  grpnnncan2  19256  imasgrp2  19274  mulgnn0ass  19329  mulgsubdir  19333  cmn32  20023  ablsubadd  20032  imasrng  20408  imasring  20569  isdomn4  20976  zntoslem  21871  xmettri3  24681  mettri3  24682  xmetrtri  24683  xmetrtri2  24684  metrtri  24685  cphdivcl  25512  cphassr  25542  relogbmulexp  27115  grpodivdiv  31151  grpomuldivass  31152  ablo32  31160  ablodivdiv4  31165  ablodiv32  31166  nvmdi  31259  dipdi  31454  dipassr  31457  dipsubdir  31459  dipsubdi  31460  dvrcan5  33846  cgr3tr4  36941  cgr3rflx  36943  endofsegid  36974  seglemin  37002  broutsideof2  37011  rngosubdi  39016  rngosubdir  39017  isdrngo2  39029  crngm23  39073  dmncan2  39148  latmassOLD  40423  latm32  40425  cvrnbtwn4  40473  cvrcmp2  40478  ltcvrntr  40618  atcvrj0  40622  3dim3  40663  paddasslem17  41030  paddass  41032  lautlt  41285  lautcvr  41286  lautj  41287  lautm  41288  erngdvlem3  42184  dvalveclem  42219  mendlmod  44328  idomcanr  49581