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

Theorem imp4a 425
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 424 . 2 ((𝜑𝜓) → ((𝜒𝜃) → 𝜏))
32ex 415 1 (𝜑 → (𝜓 → ((𝜒𝜃) → 𝜏)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 398
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 209  df-an 399
This theorem is referenced by:  imp4d  427  imp55  445  imp511  446  reuss2  4281  wefrc  5542  f1oweALT  7665  tfrlem9  8013  tz7.49  8073  oaordex  8176  dfac2b  9548  zorn2lem4  9913  zorn2lem7  9916  psslinpr  10445  facwordi  13641  ndvdssub  15752  pmtrfrn  18578  elcls  21673  elcls3  21683  neibl  23103  met2ndc  23125  itgcn  24435  branmfn  29874  atcvatlem  30154  atcvat4i  30166  umgr2cycllem  32380  satfv0fun  32611  prtlem15  36003  cvlsupr4  36473  cvlsupr5  36474  cvlsupr6  36475  2llnneN  36537  cvrat4  36571  llnexchb2  36997  cdleme48gfv1  37664  cdlemg6e  37750  dihord6apre  38384  dihord5b  38387  dihord5apre  38390  dihglblem5apreN  38419  dihglbcpreN  38428
  Copyright terms: Public domain W3C validator