Theorem 3adant3r1 1189

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

Syntax hints:   → wi 4   ∧ wa 396   ∧ w3a 1092

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 208  df-an 397  df-3an 1094

This theorem is referenced by:  dif1en  9086  ccatswrd  14622  plttr  18297  pltletr  18298  latjlej1  18410  latjlej2  18411  latnlej  18413  latnlej2  18416  latmlem2  18427  latledi  18434  latjass  18440  latj32  18442  latj13  18443  ipopos  18493  tsrlemax  18543  imasmnd2  18733  grpsubsub  18996  grpnnncan2  19004  imasgrp2  19022  mulgnn0ass  19077  mulgsubdir  19081  cmn32  19766  ablsubadd  19775  imasrng  20149  imasring  20301  isdomn4  20688  zntoslem  21531  xmettri3  24336  mettri3  24337  xmetrtri  24338  xmetrtri2  24339  metrtri  24340  cphdivcl  25167  cphassr  25197  relogbmulexp  26760  grpodivdiv  30629  grpomuldivass  30630  ablo32  30638  ablodivdiv4  30643  ablodiv32  30644  nvmdi  30737  dipdi  30932  dipassr  30935  dipsubdir  30937  dipsubdi  30938  dvrcan5  33317  cgr3tr4  36280  cgr3rflx  36282  endofsegid  36313  seglemin  36341  broutsideof2  36350  rngosubdi  38312  rngosubdir  38313  isdrngo2  38325  crngm23  38369  dmncan2  38444  latmassOLD  39721  latm32  39723  cvrnbtwn4  39771  cvrcmp2  39776  ltcvrntr  39916  atcvrj0  39920  3dim3  39961  paddasslem17  40328  paddass  40330  lautlt  40583  lautcvr  40584  lautj  40585  lautm  40586  erngdvlem3  41482  dvalveclem  41517  mendlmod  43634