![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > imp42 | Structured version Visualization version GIF version |
Description: An importation inference. (Contributed by NM, 26-Apr-1994.) |
Ref | Expression |
---|---|
imp4.1 | ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏)))) |
Ref | Expression |
---|---|
imp42 | ⊢ (((𝜑 ∧ (𝜓 ∧ 𝜒)) ∧ 𝜃) → 𝜏) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | imp4.1 | . . 3 ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏)))) | |
2 | 1 | imp32 417 | . 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: imp55 441 ltexprlem7 11076 iscatd 17681 isposd 18343 pospropd 18347 mulgghm2 21462 ordtbaslem 23180 txbas 23559 nocvxminlem 27804 frgrncvvdeqlem8 30236 grporcan 30448 chirredlem1 32320 cvxpconn 35083 cvxsconn 35084 rngonegmn1l 37655 prnc 37781 reuopreuprim 47134 uhgrimisgrgriclem 47513 |
Copyright terms: Public domain | W3C validator |