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

Theorem imp41 620
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 444 . 2 ((𝜑𝜓) → (𝜒 → (𝜃𝜏)))
32imp31 447 1 ((((𝜑𝜓) ∧ 𝜒) ∧ 𝜃) → 𝜏)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383
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 385
This theorem is referenced by:  ad4ant123OLD  1179  ad4ant124OLD  1181  ad4ant134OLD  1183  ad4ant234OLD  1185  ad4ant13OLD  1208  ad4ant14OLD  1210  ad4ant23OLD  1212  ad4ant24OLD  1214  ad5ant13OLD  1217  ad5ant14OLD  1219  ad5ant15OLD  1221  ad5ant23OLD  1223  ad5ant24OLD  1225  ad5ant25OLD  1227  3anassrs  1454  ad5ant245OLD  1456  ad5ant234OLD  1458  ad5ant235OLD  1460  ad5ant123OLD  1462  ad5ant124OLD  1464  ad5ant125  1465  ad5ant125OLD  1466  ad5ant134OLD  1468  ad5ant135OLD  1470  ad5ant145OLD  1472  ad5ant2345  1474  peano5  7254  oelim  7783  lemul12a  11073  uzwo  11944  elfznelfzo  12767  injresinj  12783  swrdswrd  13660  2cshwcshw  13771  dvdsprmpweqle  15792  catidd  16542  grpinveu  17657  2ndcctbss  21460  rusgrnumwwlks  27096  erclwwlktr  27145  erclwwlkntr  27202  grpoinveu  27682  spansncvi  28820  sumdmdii  29583  relowlpssretop  33523  matunitlindflem1  33718  unichnidl  34143  linepsubN  35541  pmapsub  35557  cdlemkid4  36724  hbtlem2  38196  ply1mulgsumlem2  42685
  Copyright terms: Public domain W3C validator