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

Theorem syl3an2 1250
 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 1180 . . 3 (𝜓 → (𝜒 → (𝜃𝜏)))
41, 3syl5 32 . 2 (𝜓 → (𝜑 → (𝜃𝜏)))
543imp 1175 1 ((𝜓𝜑𝜃) → 𝜏)
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ w3a 962 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 964 This theorem is referenced by:  syl3an2b  1253  syl3an2br  1256  syl3anl2  1265  nndi  6382  nnmass  6383  prarloclemarch2  7234  1idprl  7405  1idpru  7406  recexprlem1ssl  7448  recexprlem1ssu  7449  msqge0  8385  mulge0  8388  divsubdirap  8475  divdiv32ap  8487  peano2uz  9385  fzoshftral  10022  expdivap  10351  bcval5  10516  redivap  10653  imdivap  10660  absdiflt  10871  absdifle  10872  retanclap  11436  tannegap  11442  lcmgcdeq  11771  isprm3  11806  prmdvdsexpb  11834  cnpf2  12386  blres  12613
 Copyright terms: Public domain W3C validator