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

Theorem syl3an2 1168
Description: A syllogism inference. (Contributed by NM, 22-Aug-1995.)
Hypotheses
Ref Expression
syl3an2.1 (φχ)
syl3an2.2 ((ψ χ θ) → τ)
Assertion
Ref Expression
syl3an2 ((ψ φ θ) → τ)

Proof of Theorem syl3an2
StepHypRef Expression
1 syl3an2.1 . . 3 (φχ)
2 syl3an2.2 . . . 4 ((ψ χ θ) → τ)
323exp 1102 . . 3 (ψ → (χ → (θτ)))
41, 3syl5 28 . 2 (ψ → (φ → (θτ)))
543imp 1097 1 ((ψ φ θ) → τ)
Colors of variables: wff set class
Syntax hints:  wi 4   w3a 884
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 886
This theorem is referenced by:  syl3an2b  1171  syl3an2br  1174  syl3anl2  1183  nndi  6004  nnmass  6005  prarloclemarch2  6402  1idprl  6566  1idpru  6567  recexprlem1ssl  6605  recexprlem1ssu  6606  msqge0  7400  mulge0  7403  divsubdirap  7466  divdiv32ap  7478  peano2uz  8302  fzoshftral  8864  expdivap  8959  redivap  9102  imdivap  9109
  Copyright terms: Public domain W3C validator