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

Theorem imp4a 427
 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 426 . 2 ((𝜑𝜓) → ((𝜒𝜃) → 𝜏))
32ex 417 1 (𝜑 → (𝜓 → ((𝜒𝜃) → 𝜏)))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 400 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 210  df-an 401 This theorem is referenced by:  imp4d  429  imp55  447  imp511  448  reuss2  4218  wefrc  5519  f1oweALT  7678  tfrlem9  8032  tz7.49  8092  oaordex  8195  dfac2b  9583  zorn2lem4  9952  zorn2lem7  9955  psslinpr  10484  facwordi  13692  ndvdssub  15803  pmtrfrn  18646  elcls  21766  elcls3  21776  neibl  23196  met2ndc  23218  itgcn  24537  branmfn  29980  atcvatlem  30260  atcvat4i  30272  umgr2cycllem  32611  satfv0fun  32842  prtlem15  36444  cvlsupr4  36914  cvlsupr5  36915  cvlsupr6  36916  2llnneN  36978  cvrat4  37012  llnexchb2  37438  cdleme48gfv1  38105  cdlemg6e  38191  dihord6apre  38825  dihord5b  38828  dihord5apre  38831  dihglblem5apreN  38860  dihglbcpreN  38869
 Copyright terms: Public domain W3C validator