Theorem 3adant3r1 1180

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

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

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 206  df-an 396  df-3an 1087

This theorem is referenced by:  ccatswrd  14309  plttr  17975  pltletr  17976  latjlej1  18086  latjlej2  18087  latnlej  18089  latnlej2  18092  latmlem2  18103  latledi  18110  latjass  18116  latj32  18118  latj13  18119  ipopos  18169  tsrlemax  18219  imasmnd2  18337  grpsubsub  18579  grpnnncan2  18587  imasgrp2  18605  mulgnn0ass  18654  mulgsubdir  18658  cmn32  19320  ablsubadd  19328  imasring  19773  zntoslem  20676  xmettri3  23414  mettri3  23415  xmetrtri  23416  xmetrtri2  23417  metrtri  23418  cphdivcl  24251  cphassr  24281  relogbmulexp  25833  grpodivdiv  28803  grpomuldivass  28804  ablo32  28812  ablodivdiv4  28817  ablodiv32  28818  nvmdi  28911  dipdi  29106  dipassr  29109  dipsubdir  29111  dipsubdi  29112  dvrcan5  31392  cgr3tr4  34281  cgr3rflx  34283  endofsegid  34314  seglemin  34342  broutsideof2  34351  rngosubdi  36030  rngosubdir  36031  isdrngo2  36043  crngm23  36087  dmncan2  36162  latmassOLD  37170  latm32  37172  cvrnbtwn4  37220  cvrcmp2  37225  ltcvrntr  37365  atcvrj0  37369  3dim3  37410  paddasslem17  37777  paddass  37779  lautlt  38032  lautcvr  38033  lautj  38034  lautm  38035  erngdvlem3  38931  dvalveclem  38966  isdomn4  40100  mendlmod  40934