Theorem 3adant3r1 1184

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1087

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 1089

This theorem is referenced by:  dif1en  9098  ccatswrd  14604  plttr  18275  pltletr  18276  latjlej1  18388  latjlej2  18389  latnlej  18391  latnlej2  18394  latmlem2  18405  latledi  18412  latjass  18418  latj32  18420  latj13  18421  ipopos  18471  tsrlemax  18521  imasmnd2  18711  grpsubsub  18971  grpnnncan2  18979  imasgrp2  18997  mulgnn0ass  19052  mulgsubdir  19056  cmn32  19741  ablsubadd  19750  imasrng  20124  imasring  20278  isdomn4  20661  zntoslem  21523  xmettri3  24309  mettri3  24310  xmetrtri  24311  xmetrtri2  24312  metrtri  24313  cphdivcl  25150  cphassr  25180  relogbmulexp  26756  grpodivdiv  30628  grpomuldivass  30629  ablo32  30637  ablodivdiv4  30642  ablodiv32  30643  nvmdi  30736  dipdi  30931  dipassr  30934  dipsubdir  30936  dipsubdi  30937  dvrcan5  33330  cgr3tr4  36268  cgr3rflx  36270  endofsegid  36301  seglemin  36329  broutsideof2  36338  rngosubdi  38196  rngosubdir  38197  isdrngo2  38209  crngm23  38253  dmncan2  38328  latmassOLD  39605  latm32  39607  cvrnbtwn4  39655  cvrcmp2  39660  ltcvrntr  39800  atcvrj0  39804  3dim3  39845  paddasslem17  40212  paddass  40214  lautlt  40467  lautcvr  40468  lautj  40469  lautm  40470  erngdvlem3  41366  dvalveclem  41401  mendlmod  43546