![]() |
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-1 5 ax-2 6 ax-mp 7 |
This theorem is referenced by: mp2d 47 pm2.43a 51 embantd 56 mpan2d 420 ceqsalt 2659 rspcimdv 2737 fvimacnv 5453 riotass2 5672 pr2ne 6917 0mnnnnn0 8803 caucvgre 10545 climcn1 10867 climcn2 10868 gcdaddm 11417 dvdsgcd 11443 coprmgcdb 11512 nprm 11547 uniopn 11867 metcnp3 12308 cncfco 12359 |
Copyright terms: Public domain | W3C validator |