![]() |
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-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 |
This theorem is referenced by: eqrdav 2099 disjiun 3870 euotd 4114 onsucelsucr 4362 isotr 5649 spc2ed 6060 ltbtwnnqq 7124 genpcdl 7228 genpcuu 7229 un0addcl 8862 un0mulcl 8863 btwnnz 8997 uznfz 9724 elfz0ubfz0 9743 fzoss1 9789 elfzo0z 9802 fzofzim 9806 elfzom1p1elfzo 9832 ssfzo12bi 9843 subfzo0 9860 modfzo0difsn 10009 expaddzap 10178 caucvgre 10593 caubnd2 10729 summodc 10991 fzo0dvdseq 11350 nno 11398 lcmdvds 11553 hashgcdeq 11696 neii1 12098 neii2 12100 |
Copyright terms: Public domain | W3C validator |