![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > mpid | GIF version |
Description: A nested modus ponens deduction. (Contributed by NM, 14-Dec-2004.) |
Ref | Expression |
---|---|
mpid.1 | ⊢ (𝜑 → 𝜒) |
mpid.2 | ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃))) |
Ref | Expression |
---|---|
mpid | ⊢ (𝜑 → (𝜓 → 𝜃)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mpid.1 | . . 3 ⊢ (𝜑 → 𝜒) | |
2 | 1 | a1d 22 | . 2 ⊢ (𝜑 → (𝜓 → 𝜒)) |
3 | mpid.2 | . 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃))) | |
4 | 2, 3 | mpdd 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 |