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  9215  ccatswrd  14860  plttr  18564  pltletr  18565  latjlej1  18677  latjlej2  18678  latnlej  18680  latnlej2  18683  latmlem2  18694  latledi  18701  latjass  18707  latj32  18709  latj13  18710  ipopos  18760  tsrlemax  18810  imasmnd2  19018  grpsubsub  19289  grpnnncan2  19297  imasgrp2  19315  mulgnn0ass  19370  mulgsubdir  19374  cmn32  20065  ablsubadd  20074  imasrng  20450  imasring  20611  isdomn4  21018  zntoslem  21917  xmettri3  24727  mettri3  24728  xmetrtri  24729  xmetrtri2  24730  metrtri  24731  cphdivcl  25558  cphassr  25588  relogbmulexp  27163  grpodivdiv  31199  grpomuldivass  31200  ablo32  31208  ablodivdiv4  31213  ablodiv32  31214  nvmdi  31307  dipdi  31502  dipassr  31505  dipsubdir  31507  dipsubdi  31508  dvrcan5  33895  cgr3tr4  37032  cgr3rflx  37034  endofsegid  37065  seglemin  37093  broutsideof2  37102  rngosubdi  39145  rngosubdir  39146  isdrngo2  39158  crngm23  39202  dmncan2  39277  latmassOLD  40552  latm32  40554  cvrnbtwn4  40602  cvrcmp2  40607  ltcvrntr  40747  atcvrj0  40751  3dim3  40792  paddasslem17  41159  paddass  41161  lautlt  41414  lautcvr  41415  lautj  41416  lautm  41417  erngdvlem3  42313  dvalveclem  42348  mendlmod  44452  idomcanr  49776