| 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 115 | . . 3 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃))) |
| 3 | 2 | com23 78 | . 2 ⊢ (𝜑 → (𝜒 → (𝜓 → 𝜃))) |
| 4 | 3 | imp 124 | 1 ⊢ ((𝜑 ∧ 𝜒) → (𝜓 → 𝜃)) |
| Colors of variables: wff set class |
| Syntax hints: → wi 4 ∧ wa 104 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 |
| This theorem is referenced by: eqrdav 2203 disjiun 4038 euotd 4297 onsucelsucr 4554 isotr 5875 spc2ed 6309 nninfninc 7207 ltbtwnnqq 7510 genpcdl 7614 genpcuu 7615 un0addcl 9310 un0mulcl 9311 btwnnz 9449 uznfz 10207 elfz0ubfz0 10229 fzoss1 10276 elfzo0z 10289 fzofzim 10293 elfzom1p1elfzo 10324 ssfzo12bi 10335 subfzo0 10352 modfzo0difsn 10521 expaddzap 10709 caucvgre 11211 caubnd2 11347 summodc 11613 fzo0dvdseq 12087 nno 12136 lcmdvds 12320 hashgcdeq 12481 modprm0 12496 pcqcl 12548 issubg4m 13447 01eq0ring 13869 neii1 14537 neii2 14539 fsumcncntop 14957 gausslemma2dlem1a 15453 |
| Copyright terms: Public domain | W3C validator |