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

Theorem imp4a 422
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 421 . 2 ((𝜑𝜓) → ((𝜒𝜃) → 𝜏))
32ex 412 1 (𝜑 → (𝜓 → ((𝜒𝜃) → 𝜏)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395
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 207  df-an 396
This theorem is referenced by:  imp4d  424  imp55  442  imp511  443  reuss2  4326  wefrc  5679  f1oweALT  7997  tfrlem9  8425  tz7.49  8485  oaordex  8596  dfac2b  10171  zorn2lem4  10539  zorn2lem7  10542  psslinpr  11071  facwordi  14328  ndvdssub  16446  pmtrfrn  19476  elcls  23081  elcls3  23091  neibl  24514  met2ndc  24536  itgcn  25880  branmfn  32124  atcvatlem  32404  atcvat4i  32416  umgr2cycllem  35145  satfv0fun  35376  prtlem15  38876  cvlsupr4  39346  cvlsupr5  39347  cvlsupr6  39348  2llnneN  39411  cvrat4  39445  llnexchb2  39871  cdleme48gfv1  40538  cdlemg6e  40624  dihord6apre  41258  dihord5b  41261  dihord5apre  41264  dihglblem5apreN  41293  dihglbcpreN  41302
  Copyright terms: Public domain W3C validator