![]() |
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 422 | . 2 ⊢ ((𝜑 ∧ 𝜓) → ((𝜒 ∧ 𝜃) → 𝜏)) |
3 | 2 | ex 413 | 1 ⊢ (𝜑 → (𝜓 → ((𝜒 ∧ 𝜃) → 𝜏))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 |
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 206 df-an 397 |
This theorem is referenced by: imp4d 425 imp55 443 imp511 444 reuss2 4314 wefrc 5669 f1oweALT 7955 tfrlem9 8381 tz7.49 8441 oaordex 8554 dfac2b 10121 zorn2lem4 10490 zorn2lem7 10493 psslinpr 11022 facwordi 14245 ndvdssub 16348 pmtrfrn 19320 elcls 22568 elcls3 22578 neibl 24001 met2ndc 24023 itgcn 25353 branmfn 31345 atcvatlem 31625 atcvat4i 31637 umgr2cycllem 34119 satfv0fun 34350 prtlem15 37733 cvlsupr4 38203 cvlsupr5 38204 cvlsupr6 38205 2llnneN 38268 cvrat4 38302 llnexchb2 38728 cdleme48gfv1 39395 cdlemg6e 39481 dihord6apre 40115 dihord5b 40118 dihord5apre 40121 dihglblem5apreN 40150 dihglbcpreN 40159 |
Copyright terms: Public domain | W3C validator |