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

Theorem imp4a 612
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 611 . 2 ((𝜑𝜓) → ((𝜒𝜃) → 𝜏))
32ex 449 1 (𝜑 → (𝜓 → ((𝜒𝜃) → 𝜏)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383
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 196  df-an 385
This theorem is referenced by:  imp4bOLD  614  imp4d  616  imp55  625  imp511  626  reuss2  3866  wefrc  5032  f1oweALT  7043  tfrlem9  7368  tz7.49  7427  oaordex  7525  dfac2  8836  zorn2lem4  9204  zorn2lem7  9207  psslinpr  9732  facwordi  12938  ndvdssub  14971  pmtrfrn  17701  elcls  20687  elcls3  20697  neibl  22116  met2ndc  22138  itgcn  23415  branmfn  28348  atcvatlem  28628  atcvat4i  28640  prtlem15  33178  cvlsupr4  33650  cvlsupr5  33651  cvlsupr6  33652  2llnneN  33713  cvrat4  33747  llnexchb2  34173  cdleme48gfv1  34842  cdlemg6e  34928  dihord6apre  35563  dihord5b  35566  dihord5apre  35569  dihglblem5apreN  35598  dihglbcpreN  35607
  Copyright terms: Public domain W3C validator