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

Theorem imp41 426
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 407 . 2 ((𝜑𝜓) → (𝜒 → (𝜃𝜏)))
32imp31 418 1 ((((𝜑𝜓) ∧ 𝜒) ∧ 𝜃) → 𝜏)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396
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 208  df-an 397
This theorem is referenced by:  3anassrs  1353  ad5ant125  1359  ad5ant2345  1363  peano5  7468  oelim  8017  lemul12a  11352  uzwo  12164  elfznelfzo  12996  injresinj  13012  swrdswrd  13907  2cshwcshw  14027  dvdsprmpweqle  16055  catidd  16784  grpinveu  17899  2ndcctbss  21751  rusgrnumwwlks  27439  erclwwlktr  27486  erclwwlkntr  27536  grpoinveu  27983  spansncvi  29116  sumdmdii  29879  relowlpssretop  34197  matunitlindflem1  34440  unichnidl  34862  linepsubN  36440  pmapsub  36456  cdlemkid4  37622  hbtlem2  39230  2reu8i  42850  ply1mulgsumlem2  43943
  Copyright terms: Public domain W3C validator