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 614. (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 445 | . 2 ⊢ ((𝜑 ∧ 𝜓) → (𝜒 → (𝜃 → 𝜏))) |
3 | 2 | impd 447 | 1 ⊢ ((𝜑 ∧ 𝜓) → ((𝜒 ∧ 𝜃) → 𝜏)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 384 |
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 386 |
This theorem is referenced by: imp4a 614 imp43 621 pm2.61da3ne 2883 onmindif 5815 oaordex 7638 pssnn 8178 alephval3 8933 dfac5 8951 dfac2 8953 coftr 9095 zorn2lem6 9323 addcanpi 9721 mulcanpi 9722 ltmpi 9726 ltexprlem6 9863 axpre-sup 9990 bndndx 11291 relexpaddd 13794 dmdprdd 18398 lssssr 18953 coe1fzgsumdlem 19671 evl1gsumdlem 19720 1stcrest 21256 upgrreslem 26196 umgrreslem 26197 mdsymlem3 29264 mdsymlem6 29267 sumdmdlem 29277 mclsax 31466 mclsppslem 31480 prtlem17 34161 cvratlem 34707 paddidm 35127 pmodlem2 35133 pclfinclN 35236 icceuelpart 41372 |
Copyright terms: Public domain | W3C validator |