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 3984 euotd 4239 onsucelsucr 4492 isotr 5795 spc2ed 6212 ltbtwnnqq 7377 genpcdl 7481 genpcuu 7482 un0addcl 9168 un0mulcl 9169 btwnnz 9306 uznfz 10059 elfz0ubfz0 10081 fzoss1 10127 elfzo0z 10140 fzofzim 10144 elfzom1p1elfzo 10170 ssfzo12bi 10181 subfzo0 10198 modfzo0difsn 10351 expaddzap 10520 caucvgre 10945 caubnd2 11081 summodc 11346 fzo0dvdseq 11817 nno 11865 lcmdvds 12033 hashgcdeq 12193 modprm0 12208 pcqcl 12260 neii1 12941 neii2 12943 fsumcncntop 13350 |
Copyright terms: Public domain | W3C validator |