![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > impancom | GIF version |
Description: Mixed importation/commutation inference. (Contributed by NM, 22-Jun-2013.) |
Ref | Expression |
---|---|
impancom.1 | ⊢ ((𝜑 ∧ 𝜓) → (𝜒 → 𝜃)) |
Ref | Expression |
---|---|
impancom | ⊢ ((𝜑 ∧ 𝜒) → (𝜓 → 𝜃)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | impancom.1 | . . . 4 ⊢ ((𝜑 ∧ 𝜓) → (𝜒 → 𝜃)) | |
2 | 1 | ex 115 | . . 3 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃))) |
3 | 2 | com23 78 | . 2 ⊢ (𝜑 → (𝜒 → (𝜓 → 𝜃))) |
4 | 3 | imp 124 | 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-ia1 106 ax-ia2 107 ax-ia3 108 |
This theorem is referenced by: eqrdav 2186 disjiun 4010 euotd 4266 onsucelsucr 4519 isotr 5830 spc2ed 6247 ltbtwnnqq 7427 genpcdl 7531 genpcuu 7532 un0addcl 9222 un0mulcl 9223 btwnnz 9360 uznfz 10116 elfz0ubfz0 10138 fzoss1 10184 elfzo0z 10197 fzofzim 10201 elfzom1p1elfzo 10227 ssfzo12bi 10238 subfzo0 10255 modfzo0difsn 10408 expaddzap 10577 caucvgre 11003 caubnd2 11139 summodc 11404 fzo0dvdseq 11876 nno 11924 lcmdvds 12092 hashgcdeq 12252 modprm0 12267 pcqcl 12319 issubg4m 13082 01eq0ring 13393 neii1 13887 neii2 13889 fsumcncntop 14296 |
Copyright terms: Public domain | W3C validator |