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

Theorem mpdd 40
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-1 5  ax-2 6  ax-mp 7
This theorem is referenced by:  mpid  41  mpdi  42  syld  44  syl6c  65  mpteqb  5377  oprabid  5663  nnmordi  6255  nnmord  6256  brecop  6362  findcard2  6585  findcard2s  6586  ordiso2  6707  zindd  8834  cau3lem  10512  climcau  10700  dvdsabseq  10941
  Copyright terms: Public domain W3C validator