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 208 df-an 397 |
This theorem is referenced by: imp4d 425 imp55 443 imp511 444 reuss2 4280 wefrc 5542 f1oweALT 7662 tfrlem9 8010 tz7.49 8070 oaordex 8173 dfac2b 9544 zorn2lem4 9909 zorn2lem7 9912 psslinpr 10441 facwordi 13637 ndvdssub 15748 pmtrfrn 18515 elcls 21609 elcls3 21619 neibl 23038 met2ndc 23060 itgcn 24370 branmfn 29809 atcvatlem 30089 atcvat4i 30101 umgr2cycllem 32284 satfv0fun 32515 prtlem15 35891 cvlsupr4 36361 cvlsupr5 36362 cvlsupr6 36363 2llnneN 36425 cvrat4 36459 llnexchb2 36885 cdleme48gfv1 37552 cdlemg6e 37638 dihord6apre 38272 dihord5b 38275 dihord5apre 38278 dihglblem5apreN 38307 dihglbcpreN 38316 |
Copyright terms: Public domain | W3C validator |