![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > expcomd | GIF version |
Description: Deduction form of expcom 115. (Contributed by Alan Sare, 22-Jul-2012.) |
Ref | Expression |
---|---|
expcomd.1 | ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃)) |
Ref | Expression |
---|---|
expcomd | ⊢ (𝜑 → (𝜒 → (𝜓 → 𝜃))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | expcomd.1 | . . 3 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃)) | |
2 | 1 | expd 256 | . 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃))) |
3 | 2 | com23 78 | 1 ⊢ (𝜑 → (𝜒 → (𝜓 → 𝜃))) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 103 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia3 107 |
This theorem is referenced by: simplbi2comg 1402 2moswapdc 2065 indifdir 3298 reupick 3326 issod 4201 poxp 6083 smores2 6145 smoiun 6152 mapxpen 6695 f1dmvrnfibi 6784 recexprlemm 7377 ltleletr 7766 fzind 9067 iccid 9598 ssfzo12bi 9892 dvdsabseq 11390 divalgb 11467 cncongr1 11627 txlm 12287 blsscls2 12479 metcnpi3 12503 |
Copyright terms: Public domain | W3C validator |