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 114 | . . 3 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃))) |
3 | 2 | com23 78 | . 2 ⊢ (𝜑 → (𝜒 → (𝜓 → 𝜃))) |
4 | 3 | imp 123 | 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-ia1 105 ax-ia2 106 ax-ia3 107 |
This theorem is referenced by: eqrdav 2169 disjiun 3982 euotd 4237 onsucelsucr 4490 isotr 5792 spc2ed 6209 ltbtwnnqq 7364 genpcdl 7468 genpcuu 7469 un0addcl 9155 un0mulcl 9156 btwnnz 9293 uznfz 10046 elfz0ubfz0 10068 fzoss1 10114 elfzo0z 10127 fzofzim 10131 elfzom1p1elfzo 10157 ssfzo12bi 10168 subfzo0 10185 modfzo0difsn 10338 expaddzap 10507 caucvgre 10932 caubnd2 11068 summodc 11333 fzo0dvdseq 11804 nno 11852 lcmdvds 12020 hashgcdeq 12180 modprm0 12195 pcqcl 12247 neii1 12900 neii2 12902 fsumcncntop 13309 |
Copyright terms: Public domain | W3C validator |