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

Theorem syld3an1 1369
 Description: A syllogism inference. (Contributed by NM, 7-Jul-2008.)
Hypotheses
Ref Expression
syld3an1.1 ((𝜒𝜓𝜃) → 𝜑)
syld3an1.2 ((𝜑𝜓𝜃) → 𝜏)
Assertion
Ref Expression
syld3an1 ((𝜒𝜓𝜃) → 𝜏)

Proof of Theorem syld3an1
StepHypRef Expression
1 syld3an1.1 . . . 4 ((𝜒𝜓𝜃) → 𝜑)
213com13 1267 . . 3 ((𝜃𝜓𝜒) → 𝜑)
3 syld3an1.2 . . . 4 ((𝜑𝜓𝜃) → 𝜏)
433com13 1267 . . 3 ((𝜃𝜓𝜑) → 𝜏)
52, 4syld3an3 1368 . 2 ((𝜃𝜓𝜒) → 𝜏)
653com13 1267 1 ((𝜒𝜓𝜃) → 𝜏)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ w3a 1036 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 197  df-an 386  df-3an 1038 This theorem is referenced by:  npncan  10246  nnpcan  10248  ppncan  10267  muldivdir  10664  div2neg  10692  ltmuldiv  10840  opfi1uzind  13222  opfi1uzindOLD  13228  sgrp2nmndlem4  17336  zndvds  19817  subdivcomb1  31319  wsuceq123  31461  atlrelat1  34088  cvlatcvr1  34108  dih11  36034  mullimc  39252  mullimcf  39259  icccncfext  39404  stoweidlem34  39558  stoweidlem49  39573  stoweidlem57  39581  sigarexp  40352  el0ldepsnzr  41544
 Copyright terms: Public domain W3C validator