| 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 421 | . 2 ⊢ ((𝜑 ∧ 𝜓) → ((𝜒 ∧ 𝜃) → 𝜏)) |
| 3 | 2 | imp 406 | 1 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝜒 ∧ 𝜃)) → 𝜏) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∧ wa 395 |
| 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 207 df-an 396 |
| This theorem is referenced by: fundmen 9071 fiint 9366 fiintOLD 9367 ltexprlem6 11081 divgt0 12136 divge0 12137 le2sq2 14175 iscatd 17716 isfuncd 17910 islmodd 20864 lmodvsghm 20921 islssd 20933 basis2 22958 neindisj 23125 dvidlem 25950 spansneleq 31589 elspansn4 31592 adjmul 32111 kbass6 32140 mdsl0 32329 chirredlem1 32409 r1peuqusdeg1 35648 poimirlem29 37656 rngonegmn1r 37949 3dim1 39469 linepsubN 39754 pmapsub 39770 tgoldbach 47804 |
| Copyright terms: Public domain | W3C validator |