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 611 | . 2 ⊢ ((𝜑 ∧ 𝜓) → ((𝜒 ∧ 𝜃) → 𝜏)) |
3 | 2 | ex 449 | 1 ⊢ (𝜑 → (𝜓 → ((𝜒 ∧ 𝜃) → 𝜏))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 383 |
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 196 df-an 385 |
This theorem is referenced by: imp4bOLD 614 imp4d 616 imp55 625 imp511 626 reuss2 3866 wefrc 5032 f1oweALT 7043 tfrlem9 7368 tz7.49 7427 oaordex 7525 dfac2 8836 zorn2lem4 9204 zorn2lem7 9207 psslinpr 9732 facwordi 12938 ndvdssub 14971 pmtrfrn 17701 elcls 20687 elcls3 20697 neibl 22116 met2ndc 22138 itgcn 23415 branmfn 28348 atcvatlem 28628 atcvat4i 28640 prtlem15 33178 cvlsupr4 33650 cvlsupr5 33651 cvlsupr6 33652 2llnneN 33713 cvrat4 33747 llnexchb2 34173 cdleme48gfv1 34842 cdlemg6e 34928 dihord6apre 35563 dihord5b 35566 dihord5apre 35569 dihglblem5apreN 35598 dihglbcpreN 35607 |
Copyright terms: Public domain | W3C validator |