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 208  df-an 397
This theorem is referenced by:  imp4d  425  imp55  443  imp511  444  reuss2  4280  wefrc  5542  f1oweALT  7662  tfrlem9  8010  tz7.49  8070  oaordex  8173  dfac2b  9544  zorn2lem4  9909  zorn2lem7  9912  psslinpr  10441  facwordi  13637  ndvdssub  15748  pmtrfrn  18515  elcls  21609  elcls3  21619  neibl  23038  met2ndc  23060  itgcn  24370  branmfn  29809  atcvatlem  30089  atcvat4i  30101  umgr2cycllem  32284  satfv0fun  32515  prtlem15  35891  cvlsupr4  36361  cvlsupr5  36362  cvlsupr6  36363  2llnneN  36425  cvrat4  36459  llnexchb2  36885  cdleme48gfv1  37552  cdlemg6e  37638  dihord6apre  38272  dihord5b  38275  dihord5apre  38278  dihglblem5apreN  38307  dihglbcpreN  38316
  Copyright terms: Public domain W3C validator