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

Theorem syl3an2 1235
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 1165 . . 3 (𝜓 → (𝜒 → (𝜃𝜏)))
41, 3syl5 32 . 2 (𝜓 → (𝜑 → (𝜃𝜏)))
543imp 1160 1 ((𝜓𝜑𝜃) → 𝜏)
Colors of variables: wff set class
Syntax hints:  wi 4  w3a 947
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107
This theorem depends on definitions:  df-bi 116  df-3an 949
This theorem is referenced by:  syl3an2b  1238  syl3an2br  1241  syl3anl2  1250  nndi  6350  nnmass  6351  prarloclemarch2  7195  1idprl  7366  1idpru  7367  recexprlem1ssl  7409  recexprlem1ssu  7410  msqge0  8346  mulge0  8349  divsubdirap  8436  divdiv32ap  8448  peano2uz  9346  fzoshftral  9983  expdivap  10312  bcval5  10477  redivap  10614  imdivap  10621  absdiflt  10832  absdifle  10833  retanclap  11356  tannegap  11362  lcmgcdeq  11691  isprm3  11726  prmdvdsexpb  11754  cnpf2  12303  blres  12530
  Copyright terms: Public domain W3C validator