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  4916  relresfld  4926  relcoi1  4928  funco  5019  foimacnv  5234  fvi  5324  isoini2  5559  ovidig  5719  smores2  6013  tfrlem5  6033  snnen2og  6527  phpm  6533  fict  6536  infnfi  6563  isinfinf  6565  exmidpw  6576  djuun  6704  exmidfodomrlemr  6772  exmidfodomrlemrALT  6773  isumz  10667  alzdvds  10730  zsupcl  10818  infssuzex  10820  gcddvds  10830  dvdslegcd  10831  nnsf  11333  exmidsbthrlem  11350
  Copyright terms: Public domain W3C validator