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

Theorem syld3an3 1191
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 915 . 2 ((𝜑𝜓𝜒) → 𝜑)
2 simp2 916 . 2 ((𝜑𝜓𝜒) → 𝜓)
3 syld3an3.1 . 2 ((𝜑𝜓𝜒) → 𝜃)
4 syld3an3.2 . 2 ((𝜑𝜓𝜃) → 𝜏)
51, 2, 3, 4syl3anc 1146 1 ((𝜑𝜓𝜒) → 𝜏)
Colors of variables: wff set class
Syntax hints:  wi 4  w3a 896
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105
This theorem depends on definitions:  df-bi 114  df-3an 898
This theorem is referenced by:  syld3an1  1192  syld3an2  1193  brelrng  4592  moriotass  5523  nnncan1  7309  lediv1  7909  modqval  9268  modqvalr  9269  modqcl  9270  flqpmodeq  9271  modq0  9273  modqge0  9276  modqlt  9277  modqdiffl  9279  modqdifz  9280  modqvalp1  9287  expival  9416  bcval4  9613  dvdsmultr1  10137  dvdssub2  10141
  Copyright terms: Public domain W3C validator