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

Theorem mpsyl 64
Description: Modus ponens combined with a syllogism inference. (Contributed by Alan Sare, 20-Apr-2011.)
Hypotheses
Ref Expression
mpsyl.1 𝜑
mpsyl.2 (𝜓𝜒)
mpsyl.3 (𝜑 → (𝜒𝜃))
Assertion
Ref Expression
mpsyl (𝜓𝜃)

Proof of Theorem mpsyl
StepHypRef Expression
1 mpsyl.1 . . 3 𝜑
21a1i 9 . 2 (𝜓𝜑)
3 mpsyl.2 . 2 (𝜓𝜒)
4 mpsyl.3 . 2 (𝜑 → (𝜒𝜃))
52, 3, 4sylc 61 1 (𝜓𝜃)
Colors of variables: wff set class
Syntax hints:  wi 4
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7
This theorem is referenced by:  relcnvtr  4907  relresfld  4917  relcoi1  4919  funco  5010  foimacnv  5222  fvi  5309  isoini2  5540  ovidig  5700  smores2  5994  tfrlem5  6014  snnen2og  6508  phpm  6514  fict  6517  infnfi  6544  isinfinf  6546  exmidpw  6554  djuun  6681  exmidfodomrlemr  6749  exmidfodomrlemrALT  6750  alzdvds  10649  zsupcl  10737  infssuzex  10739  gcddvds  10749  dvdslegcd  10750  nnsf  11251  exmidsbthrlem  11268
  Copyright terms: Public domain W3C validator