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

Theorem mpsyl 65
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 62 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  5016  relresfld  5026  relcoi1  5028  funco  5121  foimacnv  5341  fvi  5432  isoini2  5674  ovidig  5842  smores2  6145  tfrlem5  6165  snnen2og  6706  phpm  6712  fict  6715  infnfi  6742  isinfinf  6744  exmidpw  6755  difinfinf  6938  enumct  6952  exmidfodomrlemr  7006  exmidfodomrlemrALT  7007  isumz  11050  fsumsersdc  11056  isumclim  11082  isumclim3  11084  alzdvds  11400  zsupcl  11488  infssuzex  11490  gcddvds  11500  dvdslegcd  11501  ennnfonelemrn  11777  ctinf  11788  strle1g  11892  metrest  12495  nnsf  12891  exmidsbthrlem  12909
  Copyright terms: Public domain W3C validator