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-1 5  ax-2 6  ax-mp 7
This theorem is referenced by:  mp2d  47  pm2.43a  51  embantd  56  mpan2d  420  ceqsalt  2659  rspcimdv  2737  fvimacnv  5453  riotass2  5672  pr2ne  6917  0mnnnnn0  8803  caucvgre  10545  climcn1  10867  climcn2  10868  gcdaddm  11417  dvdsgcd  11443  coprmgcdb  11512  nprm  11547  uniopn  11867  metcnp3  12308  cncfco  12359
  Copyright terms: Public domain W3C validator