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 1121	. 2 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)
3	2	3adantr1 1170	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  9200  ccatswrd  14706  plttr  18387  pltletr  18388  latjlej1  18498  latjlej2  18499  latnlej  18501  latnlej2  18504  latmlem2  18515  latledi  18522  latjass  18528  latj32  18530  latj13  18531  ipopos  18581  tsrlemax  18631  imasmnd2  18787  grpsubsub  19047  grpnnncan2  19055  imasgrp2  19073  mulgnn0ass  19128  mulgsubdir  19132  cmn32  19818  ablsubadd  19827  imasrng  20174  imasring  20327  isdomn4  20716  zntoslem  21575  xmettri3  24363  mettri3  24364  xmetrtri  24365  xmetrtri2  24366  metrtri  24367  cphdivcl  25216  cphassr  25246  relogbmulexp  26821  grpodivdiv  30559  grpomuldivass  30560  ablo32  30568  ablodivdiv4  30573  ablodiv32  30574  nvmdi  30667  dipdi  30862  dipassr  30865  dipsubdir  30867  dipsubdi  30868  dvrcan5  33240  cgr3tr4  36053  cgr3rflx  36055  endofsegid  36086  seglemin  36114  broutsideof2  36123  rngosubdi  37952  rngosubdir  37953  isdrngo2  37965  crngm23  38009  dmncan2  38084  latmassOLD  39230  latm32  39232  cvrnbtwn4  39280  cvrcmp2  39285  ltcvrntr  39426  atcvrj0  39430  3dim3  39471  paddasslem17  39838  paddass  39840  lautlt  40093  lautcvr  40094  lautj  40095  lautm  40096  erngdvlem3  40992  dvalveclem  41027  mendlmod  43201