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 108 | . . 3 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃))) |
3 | 2 | com23 72 | . 2 ⊢ (𝜑 → (𝜒 → (𝜓 → 𝜃))) |
4 | 3 | imp 115 | 1 ⊢ ((𝜑 ∧ 𝜒) → (𝜓 → 𝜃)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 97 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 99 ax-ia2 100 ax-ia3 101 |
This theorem is referenced by: eqrdav 2039 euotd 3991 onsucelsucr 4234 isotr 5456 ltbtwnnqq 6513 genpcdl 6617 genpcuu 6618 un0addcl 8215 un0mulcl 8216 btwnnz 8334 uznfz 8965 elfz0ubfz0 8982 fzoss1 9027 elfzo0z 9040 fzofzim 9044 elfzom1p1elfzo 9070 ssfzo12bi 9081 subfzo0 9097 expaddzap 9299 caucvgre 9580 caubnd2 9713 |
Copyright terms: Public domain | W3C validator |