![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > imp4b | Structured version Visualization version GIF version |
Description: An importation inference. (Contributed by NM, 26-Apr-1994.) Shorten imp4a 615. (Revised by Wolf Lammen, 19-Jul-2021.) |
Ref | Expression |
---|---|
imp4.1 | ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏)))) |
Ref | Expression |
---|---|
imp4b | ⊢ ((𝜑 ∧ 𝜓) → ((𝜒 ∧ 𝜃) → 𝜏)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | imp4.1 | . . 3 ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏)))) | |
2 | 1 | imp 444 | . 2 ⊢ ((𝜑 ∧ 𝜓) → (𝜒 → (𝜃 → 𝜏))) |
3 | 2 | impd 446 | 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 197 df-an 385 |
This theorem is referenced by: imp4a 615 imp43 622 pm2.61da3ne 3009 onmindif 5964 oaordex 7795 pssnn 8331 alephval3 9094 dfac5 9112 dfac2b 9114 dfac2OLD 9116 coftr 9258 zorn2lem6 9486 addcanpi 9884 mulcanpi 9885 ltmpi 9889 ltexprlem6 10026 axpre-sup 10153 bndndx 11454 relexpaddd 13964 dmdprdd 18569 lssssr 19126 coe1fzgsumdlem 19844 evl1gsumdlem 19893 1stcrest 21429 upgrreslem 26366 umgrreslem 26367 mdsymlem3 29544 mdsymlem6 29547 sumdmdlem 29557 mclsax 31744 mclsppslem 31758 prtlem17 34634 cvratlem 35179 paddidm 35599 pmodlem2 35605 pclfinclN 35708 icceuelpart 41851 |
Copyright terms: Public domain | W3C validator |