MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  syld3an1 Structured version   Visualization version   GIF version

Theorem syld3an1 1407
Description: A syllogism inference. (Contributed by NM, 7-Jul-2008.) (Proof shortened by Wolf Lammen, 26-Jun-2022.)
Hypotheses
Ref Expression
syld3an1.1 ((𝜒𝜓𝜃) → 𝜑)
syld3an1.2 ((𝜑𝜓𝜃) → 𝜏)
Assertion
Ref Expression
syld3an1 ((𝜒𝜓𝜃) → 𝜏)

Proof of Theorem syld3an1
StepHypRef Expression
1 syld3an1.1 . 2 ((𝜒𝜓𝜃) → 𝜑)
2 simp2 1134 . 2 ((𝜒𝜓𝜃) → 𝜓)
3 simp3 1135 . 2 ((𝜒𝜓𝜃) → 𝜃)
4 syld3an1.2 . 2 ((𝜑𝜓𝜃) → 𝜏)
51, 2, 3, 4syl3anc 1368 1 ((𝜒𝜓𝜃) → 𝜏)
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1084
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 210  df-an 400  df-3an 1086
This theorem is referenced by:  npncan  10900  nnpcan  10902  ppncan  10921  muldivdir  11326  subdivcomb1  11328  div2neg  11356  ltmuldiv  11506  opfi1uzind  13859  sgrp2nmndlem4  18088  zndvds  20244  wsuceq123  33209  atlrelat1  36610  cvlatcvr1  36630  dih11  38554  wessf1ornlem  41798  mullimc  42245  mullimcf  42252  icccncfext  42516  stoweidlem34  42663  stoweidlem49  42678  stoweidlem57  42686  sigarexp  43460  el0ldepsnzr  44863
  Copyright terms: Public domain W3C validator