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

Theorem mpsyl 59
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 56 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  4840  relresfld  4847  relcoi1  4849  funco  4940  foimacnv  5144  fvi  5230  isoini2  5458  ovidig  5618  smores2  5909  tfrlem5  5930  snnen2og  6322  phpm  6327  cauappcvgprlemm  6743  caucvgprlemm  6766  caucvgprprlemml  6792  caucvgsr  6886
  Copyright terms: Public domain W3C validator