| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > imp4a | Structured version Visualization version GIF version | ||
| Description: An importation inference. (Contributed by NM, 26-Apr-1994.) (Proof shortened by Wolf Lammen, 19-Jul-2021.) |
| Ref | Expression |
|---|---|
| imp4.1 | ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏)))) |
| Ref | Expression |
|---|---|
| imp4a | ⊢ (𝜑 → (𝜓 → ((𝜒 ∧ 𝜃) → 𝜏))) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | imp4.1 | . . 3 ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏)))) | |
| 2 | 1 | imp4b 421 | . 2 ⊢ ((𝜑 ∧ 𝜓) → ((𝜒 ∧ 𝜃) → 𝜏)) |
| 3 | 2 | ex 412 | 1 ⊢ (𝜑 → (𝜓 → ((𝜒 ∧ 𝜃) → 𝜏))) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∧ wa 395 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 |
| This theorem depends on definitions: df-bi 207 df-an 396 |
| This theorem is referenced by: imp4d 424 imp55 442 imp511 443 reuss2 4326 wefrc 5679 f1oweALT 7997 tfrlem9 8425 tz7.49 8485 oaordex 8596 dfac2b 10171 zorn2lem4 10539 zorn2lem7 10542 psslinpr 11071 facwordi 14328 ndvdssub 16446 pmtrfrn 19476 elcls 23081 elcls3 23091 neibl 24514 met2ndc 24536 itgcn 25880 branmfn 32124 atcvatlem 32404 atcvat4i 32416 umgr2cycllem 35145 satfv0fun 35376 prtlem15 38876 cvlsupr4 39346 cvlsupr5 39347 cvlsupr6 39348 2llnneN 39411 cvrat4 39445 llnexchb2 39871 cdleme48gfv1 40538 cdlemg6e 40624 dihord6apre 41258 dihord5b 41261 dihord5apre 41264 dihglblem5apreN 41293 dihglbcpreN 41302 |
| Copyright terms: Public domain | W3C validator |