![]() |
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 408 | . 2 ⊢ ((𝜑 ∧ 𝜓) → ((𝜒 ∧ 𝜃) → 𝜏)) |
3 | 2 | imp 393 | 1 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝜒 ∧ 𝜃)) → 𝜏) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 382 |
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 383 |
This theorem is referenced by: fundmen 8187 fiint 8397 ltexprlem6 10069 divgt0 11097 divge0 11098 le2sq2 13146 iscatd 16541 isfuncd 16732 islmodd 19079 lmodvsghm 19134 islssd 19146 basis2 20976 neindisj 21142 dvidlem 23899 spansneleq 28769 elspansn4 28772 adjmul 29291 kbass6 29320 mdsl0 29509 chirredlem1 29589 poimirlem29 33771 rngonegmn1r 34073 3dim1 35276 linepsubN 35561 pmapsub 35577 tgoldbach 42230 tgoldbachOLD 42237 |
Copyright terms: Public domain | W3C validator |