| 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 418 | . 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: imp55 442 ltexprlem7 11082 fzdif1 13645 iscatd 17716 isposd 18368 pospropd 18372 mulgghm2 21487 ordtbaslem 23196 txbas 23575 nocvxminlem 27822 frgrncvvdeqlem8 30325 grporcan 30537 chirredlem1 32409 cvxpconn 35247 cvxsconn 35248 rngonegmn1l 37948 prnc 38074 reuopreuprim 47513 uhgrimisgrgriclem 47898 |
| Copyright terms: Public domain | W3C validator |