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

Theorem imp41 618
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 445 . 2 ((𝜑𝜓) → (𝜒 → (𝜃𝜏)))
32imp31 448 1 ((((𝜑𝜓) ∧ 𝜒) ∧ 𝜃) → 𝜏)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384
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 197  df-an 386
This theorem is referenced by:  3anassrs  1287  ad4ant13  1289  ad4ant14  1290  ad4ant123  1291  ad4ant124  1292  ad4ant134  1293  ad4ant23  1294  ad4ant24  1295  ad4ant234  1296  ad5ant13  1298  ad5ant14  1299  ad5ant15  1300  ad5ant23  1301  ad5ant24  1302  ad5ant25  1303  ad5ant245  1304  ad5ant234  1305  ad5ant235  1306  ad5ant123  1307  ad5ant124  1308  ad5ant125  1309  ad5ant134  1310  ad5ant135  1311  ad5ant145  1312  ad5ant2345  1314  peano5  7051  oelim  7574  lemul12a  10841  uzwo  11711  elfznelfzo  12530  injresinj  12545  swrdswrd  13414  2cshwcshw  13524  dvdsprmpweqle  15533  catidd  16281  grpinveu  17396  2ndcctbss  21198  rusgrnumwwlks  26770  erclwwlkstr  26836  erclwwlksntr  26848  frgrncvvdeqlemB  27069  grpoinveu  27261  spansncvi  28399  sumdmdii  29162  relowlpssretop  32883  matunitlindflem1  33076  unichnidl  33501  linepsubN  34557  pmapsub  34573  cdlemkid4  35741  hbtlem2  37214  ply1mulgsumlem2  41493
  Copyright terms: Public domain W3C validator