![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > expcomd | GIF version |
Description: Deduction form of expcom 116. (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 258 | . 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃))) |
3 | 2 | com23 78 | 1 ⊢ (𝜑 → (𝜒 → (𝜓 → 𝜃))) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 104 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia3 108 |
This theorem is referenced by: simplbi2comg 1443 2moswapdc 2116 indifdir 3391 reupick 3419 issod 4316 poxp 6227 smores2 6289 smoiun 6296 mapxpen 6842 f1dmvrnfibi 6937 recexprlemm 7614 ltleletr 8029 fzind 9357 iccid 9912 ssfzo12bi 10211 dvdsabseq 11836 divalgb 11913 cncongr1 12086 difsqpwdvds 12320 txlm 13446 blsscls2 13660 metcnpi3 13684 |
Copyright terms: Public domain | W3C validator |