Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  imp41 Structured version   Visualization version   GIF version

Theorem imp41 429
 Description: An importation inference. (Contributed by NM, 26-Apr-1994.)
Hypothesis
Ref Expression
imp4.1 (𝜑 → (𝜓 → (𝜒 → (𝜃𝜏))))
Assertion
Ref Expression
imp41 ((((𝜑𝜓) ∧ 𝜒) ∧ 𝜃) → 𝜏)

Proof of Theorem imp41
StepHypRef Expression
1 imp4.1 . . 3 (𝜑 → (𝜓 → (𝜒 → (𝜃𝜏))))
21imp 410 . 2 ((𝜑𝜓) → (𝜒 → (𝜃𝜏)))
32imp31 421 1 ((((𝜑𝜓) ∧ 𝜒) ∧ 𝜃) → 𝜏)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 399 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 210  df-an 400 This theorem is referenced by:  3anassrs  1357  ad5ant125  1363  ad5ant2345  1367  peano5  7598  oelim  8160  lemul12a  11505  uzwo  12319  elfznelfzo  13157  injresinj  13173  swrdswrd  14078  2cshwcshw  14198  dvdsprmpweqle  16232  catidd  16963  grpinveu  18151  2ndcctbss  22101  rusgrnumwwlks  27804  erclwwlktr  27851  wwlksext2clwwlk  27886  erclwwlkntr  27900  grpoinveu  28346  spansncvi  29479  sumdmdii  30242  relowlpssretop  34932  matunitlindflem1  35204  unichnidl  35620  linepsubN  37199  pmapsub  37215  cdlemkid4  38381  hbtlem2  40239  2reu8i  43837  ply1mulgsumlem2  44962
 Copyright terms: Public domain W3C validator