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  2763  rspcimdv  2842  fvimacnv  5631  riotass2  5856  pr2ne  7190  0mnnnnn0  9207  caucvgre  10989  climcn1  11315  climcn2  11316  gcdaddm  11984  dvdsgcd  12012  coprmgcdb  12087  nprm  12122  pcqmul  12302  grpid  12911  uniopn  13471  metcnp3  13981  cncfco  14048
  Copyright terms: Public domain W3C validator