MPE Home 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  1362  ad5ant125  1368  ad5ant2345  1372  peano5  7671  peano5OLD  7672  oelim  8261  lemul12a  11690  uzwo  12507  elfznelfzo  13347  injresinj  13363  swrdswrd  14270  2cshwcshw  14390  dvdsprmpweqle  16439  catidd  17183  grpinveu  18402  2ndcctbss  22352  rusgrnumwwlks  28058  erclwwlktr  28105  wwlksext2clwwlk  28140  erclwwlkntr  28154  grpoinveu  28600  spansncvi  29733  sumdmdii  30496  relowlpssretop  35272  matunitlindflem1  35510  unichnidl  35926  linepsubN  37503  pmapsub  37519  cdlemkid4  38685  hbtlem2  40652  2reu8i  44277  ply1mulgsumlem2  45401
  Copyright terms: Public domain W3C validator