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 423. (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 407 | . 2 ⊢ ((𝜑 ∧ 𝜓) → (𝜒 → (𝜃 → 𝜏))) |
3 | 2 | impd 411 | 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: imp4a 423 imp43 428 imp5g 442 pm2.61da3ne 3103 onmindif 6273 oaordex 8173 pssnn 8724 alephval3 9524 dfac5 9542 dfac2b 9544 coftr 9683 zorn2lem6 9911 addcanpi 10309 mulcanpi 10310 ltmpi 10314 ltexprlem6 10451 axpre-sup 10579 bndndx 11884 relexpaddd 14401 dmdprdd 19050 lssssr 19654 coe1fzgsumdlem 20397 evl1gsumdlem 20447 1stcrest 21989 upgrreslem 27013 umgrreslem 27014 mdsymlem3 30109 mdsymlem6 30112 sumdmdlem 30122 mclsax 32713 mclsppslem 32727 prtlem17 35892 cvratlem 36437 paddidm 36857 pmodlem2 36863 pclfinclN 36966 icceuelpart 43473 |
Copyright terms: Public domain | W3C validator |