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

Theorem syl3an2 1204
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 1138 . . 3 (𝜓 → (𝜒 → (𝜃𝜏)))
41, 3syl5 32 . 2 (𝜓 → (𝜑 → (𝜃𝜏)))
543imp 1133 1 ((𝜓𝜑𝜃) → 𝜏)
Colors of variables: wff set class
Syntax hints:  wi 4  w3a 920
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 922
This theorem is referenced by:  syl3an2b  1207  syl3an2br  1210  syl3anl2  1219  nndi  6179  nnmass  6180  prarloclemarch2  6881  1idprl  7052  1idpru  7053  recexprlem1ssl  7095  recexprlem1ssu  7096  msqge0  7993  mulge0  7996  divsubdirap  8073  divdiv32ap  8085  peano2uz  8966  fzoshftral  9538  expdivap  9843  ibcval5  10006  redivap  10135  imdivap  10142  absdiflt  10352  absdifle  10353  lcmgcdeq  10845  isprm3  10880  prmdvdsexpb  10908
  Copyright terms: Public domain W3C validator