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  428  ceqsalt  2778  rspcimdv  2857  fvimacnv  5651  riotass2  5877  pr2ne  7220  0mnnnnn0  9237  caucvgre  11021  climcn1  11347  climcn2  11348  gcdaddm  12016  dvdsgcd  12044  coprmgcdb  12119  nprm  12154  pcqmul  12334  grpid  12980  uniopn  13953  metcnp3  14463  cncfco  14530
  Copyright terms: Public domain W3C validator