![]() |
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 2764 rspcimdv 2843 fvimacnv 5632 riotass2 5857 pr2ne 7191 0mnnnnn0 9208 caucvgre 10990 climcn1 11316 climcn2 11317 gcdaddm 11985 dvdsgcd 12013 coprmgcdb 12088 nprm 12123 pcqmul 12303 grpid 12912 uniopn 13504 metcnp3 14014 cncfco 14081 |
Copyright terms: Public domain | W3C validator |