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

Theorem syl3an2 1169
 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 1103 . . 3 (𝜓 → (𝜒 → (𝜃𝜏)))
41, 3syl5 28 . 2 (𝜓 → (𝜑 → (𝜃𝜏)))
543imp 1098 1 ((𝜓𝜑𝜃) → 𝜏)
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ w3a 885 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 887 This theorem is referenced by:  syl3an2b  1172  syl3an2br  1175  syl3anl2  1184  nndi  6065  nnmass  6066  prarloclemarch2  6517  1idprl  6688  1idpru  6689  recexprlem1ssl  6731  recexprlem1ssu  6732  msqge0  7607  mulge0  7610  divsubdirap  7684  divdiv32ap  7696  peano2uz  8526  fzoshftral  9094  expdivap  9305  redivap  9474  imdivap  9481  absdiflt  9688  absdifle  9689
 Copyright terms: Public domain W3C validator