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

Theorem syld3an3 1180
 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 904 . 2 ((𝜑𝜓𝜒) → 𝜑)
2 simp2 905 . 2 ((𝜑𝜓𝜒) → 𝜓)
3 syld3an3.1 . 2 ((𝜑𝜓𝜒) → 𝜃)
4 syld3an3.2 . 2 ((𝜑𝜓𝜃) → 𝜏)
51, 2, 3, 4syl3anc 1135 1 ((𝜑𝜓𝜒) → 𝜏)
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ w3a 885 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101 This theorem depends on definitions:  df-bi 110  df-3an 887 This theorem is referenced by:  syld3an1  1181  syld3an2  1182  brelrng  4565  moriotass  5496  nnncan1  7247  lediv1  7835  modqval  9166  modqvalr  9167  modqcl  9168  flqpmodeq  9169  modq0  9171  modqge0  9174  modqlt  9175  modqdiffl  9177  modqdifz  9178  expival  9257
 Copyright terms: Public domain W3C validator