![]() |
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 421. (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 405 | . 2 ⊢ ((𝜑 ∧ 𝜓) → (𝜒 → (𝜃 → 𝜏))) |
3 | 2 | impd 409 | 1 ⊢ ((𝜑 ∧ 𝜓) → ((𝜒 ∧ 𝜃) → 𝜏)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 394 |
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 395 |
This theorem is referenced by: imp4a 421 imp43 426 imp5g 440 pm2.61da3ne 3020 onmindif 6463 oaordex 8579 pssnn 9196 pssnnOLD 9293 alephval3 10140 dfac5 10158 dfac2b 10160 coftr 10303 zorn2lem6 10531 addcanpi 10929 mulcanpi 10930 ltmpi 10934 ltexprlem6 11071 axpre-sup 11199 bndndx 12509 dmdprdd 19973 lssssr 20855 coe1fzgsumdlem 22252 evl1gsumdlem 22305 1stcrest 23406 upgrreslem 29194 umgrreslem 29195 mdsymlem3 32292 mdsymlem6 32295 sumdmdlem 32305 mclsax 35312 mclsppslem 35326 disjlem17 38403 prtlem17 38480 cvratlem 39026 paddidm 39446 pmodlem2 39452 pclfinclN 39555 onexoegt 42816 icceuelpart 46915 |
Copyright terms: Public domain | W3C validator |