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

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

Proof of Theorem mpid
StepHypRef Expression
1 mpid.1 . . 3 (𝜑𝜒)
21a1d 22 . 2 (𝜑 → (𝜓𝜒))
3 mpid.2 . 2 (𝜑 → (𝜓 → (𝜒𝜃)))
42, 3mpdd 41 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:  mp2d  47  pm2.43a  51  embantd  56  mpan2d  424  ceqsalt  2712  rspcimdv  2790  fvimacnv  5535  riotass2  5756  pr2ne  7053  0mnnnnn0  9021  caucvgre  10765  climcn1  11089  climcn2  11090  gcdaddm  11683  dvdsgcd  11711  coprmgcdb  11780  nprm  11815  uniopn  12182  metcnp3  12694  cncfco  12761
  Copyright terms: Public domain W3C validator