![]() |
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 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 |