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-mp 5 ax-1 6 ax-2 7 ax-ia3 107 |
This theorem is referenced by: simplbi2comg 1430 2moswapdc 2103 indifdir 3373 reupick 3401 issod 4291 poxp 6191 smores2 6253 smoiun 6260 mapxpen 6805 f1dmvrnfibi 6900 recexprlemm 7556 ltleletr 7971 fzind 9297 iccid 9852 ssfzo12bi 10150 dvdsabseq 11770 divalgb 11847 cncongr1 12014 difsqpwdvds 12248 txlm 12826 blsscls2 13040 metcnpi3 13064 |
Copyright terms: Public domain | W3C validator |