![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > imp43 | Structured version Visualization version GIF version |
Description: An importation inference. (Contributed by NM, 26-Apr-1994.) |
Ref | Expression |
---|---|
imp4.1 | ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏)))) |
Ref | Expression |
---|---|
imp43 | ⊢ (((𝜑 ∧ 𝜓) ∧ (𝜒 ∧ 𝜃)) → 𝜏) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | imp4.1 | . . 3 ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏)))) | |
2 | 1 | imp4b 420 | . 2 ⊢ ((𝜑 ∧ 𝜓) → ((𝜒 ∧ 𝜃) → 𝜏)) |
3 | 2 | imp 405 | 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: fundmen 9056 fiint 9350 ltexprlem6 11066 divgt0 12115 divge0 12116 le2sq2 14135 iscatd 17656 isfuncd 17854 islmodd 20761 lmodvsghm 20818 islssd 20831 basis2 22898 neindisj 23065 dvidlem 25888 spansneleq 31452 elspansn4 31455 adjmul 31974 kbass6 32003 mdsl0 32192 chirredlem1 32272 poimirlem29 37253 rngonegmn1r 37546 3dim1 39070 linepsubN 39355 pmapsub 39371 tgoldbach 47294 |
Copyright terms: Public domain | W3C validator |