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

Theorem mpdd 36
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 23 . 2 (φ → ((ψχ) → (ψθ)))
41, 3mpd 13 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:  mpid  37  mpdi  38  syld  40  syl6c  60  mpteqb  5204  oprabid  5480  nnmordi  6025  nnmord  6026  brecop  6132  zindd  8132
  Copyright terms: Public domain W3C validator