![]() |
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 3393 reupick 3421 issod 4321 poxp 6235 smores2 6297 smoiun 6304 mapxpen 6850 f1dmvrnfibi 6945 recexprlemm 7625 ltleletr 8041 fzind 9370 iccid 9927 ssfzo12bi 10227 dvdsabseq 11855 divalgb 11932 cncongr1 12105 difsqpwdvds 12339 lss1d 13475 txlm 13818 blsscls2 14032 metcnpi3 14056 |
Copyright terms: Public domain | W3C validator |