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

Theorem syld3an1 1410
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 1137 . 2 ((𝜒𝜓𝜃) → 𝜓)
3 simp3 1138 . 2 ((𝜒𝜓𝜃) → 𝜃)
4 syld3an1.2 . 2 ((𝜑𝜓𝜃) → 𝜏)
51, 2, 3, 4syl3anc 1371 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 206  df-an 397  df-3an 1089
This theorem is referenced by:  f1dom2g  8916  f1domfi2  9136  entrfi  9144  entrfir  9145  domtrfil  9146  domtrfi  9147  domtrfir  9148  php3  9163  findcard3  9236  npncan  11431  nnpcan  11433  ppncan  11452  muldivdir  11857  subdivcomb1  11859  div2neg  11887  ltmuldiv  12037  opfi1uzind  14412  sgrp2nmndlem4  18752  zndvds  20993  wsuceq123  34475  atlrelat1  37856  cvlatcvr1  37876  dih11  39801  wessf1ornlem  43525  mullimc  43977  mullimcf  43984  icccncfext  44248  stoweidlem34  44395  stoweidlem49  44410  stoweidlem57  44418  sigarexp  45220  f1ocof1ob  45433  el0ldepsnzr  46668
  Copyright terms: Public domain W3C validator