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

Theorem mpdd 41
Description: A nested modus ponens deduction. (Contributed by NM, 12-Dec-2004.)
Hypotheses
Ref Expression
mpdd.1 (𝜑 → (𝜓𝜒))
mpdd.2 (𝜑 → (𝜓 → (𝜒𝜃)))
Assertion
Ref Expression
mpdd (𝜑 → (𝜓𝜃))

Proof of Theorem mpdd
StepHypRef Expression
1 mpdd.1 . 2 (𝜑 → (𝜓𝜒))
2 mpdd.2 . . 3 (𝜑 → (𝜓 → (𝜒𝜃)))
32a2d 26 . 2 (𝜑 → ((𝜓𝜒) → (𝜓𝜃)))
41, 3mpd 13 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:  mpid  42  mpdi  43  syld  45  syl6c  66  mpteqb  5602  oprabid  5901  nnmordi  6511  nnmord  6512  brecop  6619  findcard2  6883  findcard2s  6884  ordiso2  7028  zindd  9360  cau3lem  11107  climcau  11339  dvdsabseq  11836  metrest  13673  bj-charfunr  14218
  Copyright terms: Public domain W3C validator