ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  syld3an3 GIF version

Theorem syld3an3 1215
Description: A syllogism inference. (Contributed by NM, 20-May-2007.)
Hypotheses
Ref Expression
syld3an3.1 ((𝜑𝜓𝜒) → 𝜃)
syld3an3.2 ((𝜑𝜓𝜃) → 𝜏)
Assertion
Ref Expression
syld3an3 ((𝜑𝜓𝜒) → 𝜏)

Proof of Theorem syld3an3
StepHypRef Expression
1 simp1 939 . 2 ((𝜑𝜓𝜒) → 𝜑)
2 simp2 940 . 2 ((𝜑𝜓𝜒) → 𝜓)
3 syld3an3.1 . 2 ((𝜑𝜓𝜒) → 𝜃)
4 syld3an3.2 . 2 ((𝜑𝜓𝜃) → 𝜏)
51, 2, 3, 4syl3anc 1170 1 ((𝜑𝜓𝜒) → 𝜏)
Colors of variables: wff set class
Syntax hints:  wi 4  w3a 920
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106
This theorem depends on definitions:  df-bi 115  df-3an 922
This theorem is referenced by:  syld3an1  1216  syld3an2  1217  brelrng  4624  moriotass  5575  nnncan1  7621  lediv1  8224  modqval  9620  modqvalr  9621  modqcl  9622  flqpmodeq  9623  modq0  9625  modqge0  9628  modqlt  9629  modqdiffl  9631  modqdifz  9632  modqvalp1  9639  expival  9794  bcval4  9995  dvdsmultr1  10614  dvdssub2  10618  divalglemeuneg  10703  ndvdsadd  10711
  Copyright terms: Public domain W3C validator