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

Theorem syld3an1 1412
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 1138 . 2 ((𝜒𝜓𝜃) → 𝜓)
3 simp3 1139 . 2 ((𝜒𝜓𝜃) → 𝜃)
4 syld3an1.2 . 2 ((𝜑𝜓𝜃) → 𝜏)
51, 2, 3, 4syl3anc 1373 1 ((𝜒𝜓𝜃) → 𝜏)
Colors of variables: wff setvar class
Syntax hints:  wi 4  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:  f1dom2g  9010  f1domfi2  9222  entrfi  9230  entrfir  9231  domtrfil  9232  domtrfi  9233  domtrfir  9234  php3  9249  findcard3  9318  npncan  11530  nnpcan  11532  ppncan  11551  muldivdir  11960  subdivcomb1  11962  div2neg  11990  ltmuldiv  12141  opfi1uzind  14550  sgrp2nmndlem4  18941  zndvds  21568  wsuceq123  35815  atlrelat1  39322  cvlatcvr1  39342  dih11  41267  wessf1ornlem  45190  mullimc  45631  mullimcf  45638  icccncfext  45902  stoweidlem34  46049  stoweidlem49  46064  stoweidlem57  46072  sigarexp  46874  f1ocof1ob  47093  el0ldepsnzr  48384
  Copyright terms: Public domain W3C validator