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 113 | . . 3 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃))) |
3 | 2 | com23 77 | . 2 ⊢ (𝜑 → (𝜒 → (𝜓 → 𝜃))) |
4 | 3 | imp 122 | 1 ⊢ ((𝜑 ∧ 𝜒) → (𝜓 → 𝜃)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 102 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 104 ax-ia2 105 ax-ia3 106 |
This theorem is referenced by: eqrdav 2080 euotd 4009 onsucelsucr 4252 isotr 5476 spc2ed 5874 ltbtwnnqq 6605 genpcdl 6709 genpcuu 6710 un0addcl 8321 un0mulcl 8322 btwnnz 8441 uznfz 9120 elfz0ubfz0 9136 fzoss1 9180 elfzo0z 9193 fzofzim 9197 elfzom1p1elfzo 9223 ssfzo12bi 9234 subfzo0 9251 modfzo0difsn 9397 expaddzap 9520 caucvgre 9867 caubnd2 10003 fzo0dvdseq 10257 nno 10306 lcmdvds 10461 |
Copyright terms: Public domain | W3C validator |