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

Theorem syl3an2 1283
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 1204 . . 3 (𝜓 → (𝜒 → (𝜃𝜏)))
41, 3syl5 32 . 2 (𝜓 → (𝜑 → (𝜃𝜏)))
543imp 1195 1 ((𝜓𝜑𝜃) → 𝜏)
Colors of variables: wff set class
Syntax hints:  wi 4  w3a 980
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108
This theorem depends on definitions:  df-bi 117  df-3an 982
This theorem is referenced by:  syl3an2b  1286  syl3an2br  1289  syl3anl2  1298  nndi  6506  nnmass  6507  prarloclemarch2  7443  1idprl  7614  1idpru  7615  recexprlem1ssl  7657  recexprlem1ssu  7658  msqge0  8598  mulge0  8601  divsubdirap  8690  divdiv32ap  8702  peano2uz  9608  fzoshftral  10263  expdivap  10597  bcval5  10770  redivap  10910  imdivap  10917  absdiflt  11128  absdifle  11129  retanclap  11757  tannegap  11763  lcmgcdeq  12110  isprm3  12145  prmdvdsexpb  12176  dvdsprmpweqnn  12363  mulgaddcomlem  13078  mulginvcom  13080  cnpf2  14144  blres  14371
  Copyright terms: Public domain W3C validator