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

Theorem imp41 412
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 393 . 2 ((𝜑𝜓) → (𝜒 → (𝜃𝜏)))
32imp31 404 1 ((((𝜑𝜓) ∧ 𝜒) ∧ 𝜃) → 𝜏)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382
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 383
This theorem is referenced by:  ad4ant123OLD  1177  ad4ant124OLD  1179  ad4ant134OLD  1181  ad4ant234OLD  1183  ad4ant13OLD  1206  ad4ant14OLD  1208  ad4ant23OLD  1210  ad4ant24OLD  1212  ad5ant13OLD  1215  ad5ant14OLD  1217  ad5ant15OLD  1219  ad5ant23OLD  1221  ad5ant24OLD  1223  ad5ant25OLD  1225  3anassrs  1452  ad5ant245OLD  1454  ad5ant234OLD  1456  ad5ant235OLD  1458  ad5ant123OLD  1460  ad5ant124OLD  1462  ad5ant125  1463  ad5ant125OLD  1464  ad5ant134OLD  1466  ad5ant135OLD  1468  ad5ant145OLD  1470  ad5ant2345  1472  peano5  7235  oelim  7767  lemul12a  11082  uzwo  11953  elfznelfzo  12780  injresinj  12796  swrdswrd  13668  2cshwcshw  13779  dvdsprmpweqle  15796  catidd  16547  grpinveu  17663  2ndcctbss  21478  rusgrnumwwlks  27120  erclwwlktr  27169  erclwwlkntr  27226  grpoinveu  27707  spansncvi  28845  sumdmdii  29608  relowlpssretop  33542  matunitlindflem1  33731  unichnidl  34155  linepsubN  35553  pmapsub  35569  cdlemkid4  36736  hbtlem2  38213  ply1mulgsumlem2  42693
  Copyright terms: Public domain W3C validator