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 611 | . 2 ⊢ ((𝜑 ∧ 𝜓) → ((𝜒 ∧ 𝜃) → 𝜏)) |
3 | 2 | imp 444 | 1 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝜒 ∧ 𝜃)) → 𝜏) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 383 |
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 196 df-an 385 |
This theorem is referenced by: fundmen 7916 fiint 8122 ltexprlem6 9742 divgt0 10770 divge0 10771 le2sq2 12801 iscatd 16157 isfuncd 16348 islmodd 18692 lmodvsghm 18747 islssd 18757 basis2 20566 neindisj 20731 dvidlem 23485 spansneleq 27813 elspansn4 27816 adjmul 28335 kbass6 28364 mdsl0 28553 chirredlem1 28633 poimirlem29 32608 rngonegmn1r 32911 3dim1 33771 linepsubN 34056 pmapsub 34072 tgoldbach 40232 tgoldbachOLD 40239 |
Copyright terms: Public domain | W3C validator |