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

Theorem imp4a 423
Description: An importation inference. (Contributed by NM, 26-Apr-1994.) (Proof shortened by Wolf Lammen, 19-Jul-2021.)
Hypothesis
Ref Expression
imp4.1 (𝜑 → (𝜓 → (𝜒 → (𝜃𝜏))))
Assertion
Ref Expression
imp4a (𝜑 → (𝜓 → ((𝜒𝜃) → 𝜏)))

Proof of Theorem imp4a
StepHypRef Expression
1 imp4.1 . . 3 (𝜑 → (𝜓 → (𝜒 → (𝜃𝜏))))
21imp4b 422 . 2 ((𝜑𝜓) → ((𝜒𝜃) → 𝜏))
32ex 413 1 (𝜑 → (𝜓 → ((𝜒𝜃) → 𝜏)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396
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 206  df-an 397
This theorem is referenced by:  imp4d  425  imp55  443  imp511  444  reuss2  4314  wefrc  5669  f1oweALT  7955  tfrlem9  8381  tz7.49  8441  oaordex  8554  dfac2b  10121  zorn2lem4  10490  zorn2lem7  10493  psslinpr  11022  facwordi  14245  ndvdssub  16348  pmtrfrn  19320  elcls  22568  elcls3  22578  neibl  24001  met2ndc  24023  itgcn  25353  branmfn  31345  atcvatlem  31625  atcvat4i  31637  umgr2cycllem  34119  satfv0fun  34350  prtlem15  37733  cvlsupr4  38203  cvlsupr5  38204  cvlsupr6  38205  2llnneN  38268  cvrat4  38302  llnexchb2  38728  cdleme48gfv1  39395  cdlemg6e  39481  dihord6apre  40115  dihord5b  40118  dihord5apre  40121  dihglblem5apreN  40150  dihglbcpreN  40159
  Copyright terms: Public domain W3C validator