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

Theorem syl3an2 1208
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 1142 . . 3 (𝜓 → (𝜒 → (𝜃𝜏)))
41, 3syl5 32 . 2 (𝜓 → (𝜑 → (𝜃𝜏)))
543imp 1137 1 ((𝜓𝜑𝜃) → 𝜏)
Colors of variables: wff set class
Syntax hints:  wi 4  w3a 924
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 926
This theorem is referenced by:  syl3an2b  1211  syl3an2br  1214  syl3anl2  1223  nndi  6229  nnmass  6230  prarloclemarch2  6957  1idprl  7128  1idpru  7129  recexprlem1ssl  7171  recexprlem1ssu  7172  msqge0  8069  mulge0  8072  divsubdirap  8149  divdiv32ap  8161  peano2uz  9040  fzoshftral  9614  expdivap  9971  ibcval5  10136  redivap  10273  imdivap  10280  absdiflt  10490  absdifle  10491  lcmgcdeq  11158  isprm3  11193  prmdvdsexpb  11221
  Copyright terms: Public domain W3C validator