Theorem 3adant3r1 1183

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

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

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 1088

This theorem is referenced by:  dif1en  9086  ccatswrd  14592  plttr  18263  pltletr  18264  latjlej1  18376  latjlej2  18377  latnlej  18379  latnlej2  18382  latmlem2  18393  latledi  18400  latjass  18406  latj32  18408  latj13  18409  ipopos  18459  tsrlemax  18509  imasmnd2  18699  grpsubsub  18959  grpnnncan2  18967  imasgrp2  18985  mulgnn0ass  19040  mulgsubdir  19044  cmn32  19729  ablsubadd  19738  imasrng  20112  imasring  20266  isdomn4  20649  zntoslem  21511  xmettri3  24297  mettri3  24298  xmetrtri  24299  xmetrtri2  24300  metrtri  24301  cphdivcl  25138  cphassr  25168  relogbmulexp  26744  grpodivdiv  30615  grpomuldivass  30616  ablo32  30624  ablodivdiv4  30629  ablodiv32  30630  nvmdi  30723  dipdi  30918  dipassr  30921  dipsubdir  30923  dipsubdi  30924  dvrcan5  33318  cgr3tr4  36246  cgr3rflx  36248  endofsegid  36279  seglemin  36307  broutsideof2  36316  rngosubdi  38146  rngosubdir  38147  isdrngo2  38159  crngm23  38203  dmncan2  38278  latmassOLD  39489  latm32  39491  cvrnbtwn4  39539  cvrcmp2  39544  ltcvrntr  39684  atcvrj0  39688  3dim3  39729  paddasslem17  40096  paddass  40098  lautlt  40351  lautcvr  40352  lautj  40353  lautm  40354  erngdvlem3  41250  dvalveclem  41285  mendlmod  43431