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-mp 5  ax-1 6  ax-2 7 This theorem is referenced by:  relcnvtr  5104  relresfld  5114  relcoi1  5116  funco  5209  foimacnv  5431  fvi  5524  isoini2  5766  ovidig  5935  smores2  6238  tfrlem5  6258  snnen2og  6801  phpm  6807  fict  6810  infnfi  6837  isinfinf  6839  exmidpw  6850  difinfinf  7039  enumct  7053  exmidfodomrlemr  7131  exmidfodomrlemrALT  7132  isumz  11279  fsumsersdc  11285  isumclim  11311  isumclim3  11313  zprodap0  11471  alzdvds  11738  zsupcl  11826  infssuzex  11828  gcddvds  11838  dvdslegcd  11839  ennnfonelemrn  12131  ctinf  12142  strle1g  12251  metrest  12877  dvef  13059  bj-charfunbi  13357  pw1nct  13546  nnsf  13548  exmidsbthrlem  13564
 Copyright terms: Public domain W3C validator