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  7036  oelim  7559  lemul12a  10825  uzwo  11695  elfznelfzo  12514  injresinj  12529  swrdswrd  13398  2cshwcshw  13508  dvdsprmpweqle  15514  catidd  16262  grpinveu  17377  2ndcctbss  21168  rusgrnumwwlks  26736  erclwwlkstr  26802  erclwwlksntr  26814  frgrncvvdeqlemB  27035  grpoinveu  27222  spansncvi  28360  sumdmdii  29123  relowlpssretop  32844  matunitlindflem1  33037  unichnidl  33462  linepsubN  34518  pmapsub  34534  cdlemkid4  35702  hbtlem2  37175  ply1mulgsumlem2  41463
  Copyright terms: Public domain W3C validator