![]() |
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 425 ceqsalt 2715 rspcimdv 2794 fvimacnv 5543 riotass2 5764 pr2ne 7065 0mnnnnn0 9033 caucvgre 10785 climcn1 11109 climcn2 11110 gcdaddm 11708 dvdsgcd 11736 coprmgcdb 11805 nprm 11840 uniopn 12207 metcnp3 12719 cncfco 12786 |
Copyright terms: Public domain | W3C validator |