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  9090  ccatswrd  14625  plttr  18300  pltletr  18301  latjlej1  18413  latjlej2  18414  latnlej  18416  latnlej2  18419  latmlem2  18430  latledi  18437  latjass  18443  latj32  18445  latj13  18446  ipopos  18496  tsrlemax  18546  imasmnd2  18736  grpsubsub  18999  grpnnncan2  19007  imasgrp2  19025  mulgnn0ass  19080  mulgsubdir  19084  cmn32  19769  ablsubadd  19778  imasrng  20152  imasring  20304  isdomn4  20687  zntoslem  21549  xmettri3  24331  mettri3  24332  xmetrtri  24333  xmetrtri2  24334  metrtri  24335  cphdivcl  25162  cphassr  25192  relogbmulexp  26758  grpodivdiv  30629  grpomuldivass  30630  ablo32  30638  ablodivdiv4  30643  ablodiv32  30644  nvmdi  30737  dipdi  30932  dipassr  30935  dipsubdir  30937  dipsubdi  30938  dvrcan5  33315  cgr3tr4  36253  cgr3rflx  36255  endofsegid  36286  seglemin  36314  broutsideof2  36323  rngosubdi  38283  rngosubdir  38284  isdrngo2  38296  crngm23  38340  dmncan2  38415  latmassOLD  39692  latm32  39694  cvrnbtwn4  39742  cvrcmp2  39747  ltcvrntr  39887  atcvrj0  39891  3dim3  39932  paddasslem17  40299  paddass  40301  lautlt  40554  lautcvr  40555  lautj  40556  lautm  40557  erngdvlem3  41453  dvalveclem  41488  mendlmod  43638