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

Theorem imp4a 613
 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 612 . 2 ((𝜑𝜓) → ((𝜒𝜃) → 𝜏))
32ex 450 1 (𝜑 → (𝜓 → ((𝜒𝜃) → 𝜏)))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 384 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 197  df-an 386 This theorem is referenced by:  imp4bOLD  615  imp4d  617  imp55  626  imp511  627  reuss2  3889  wefrc  5078  f1oweALT  7112  tfrlem9  7441  tz7.49  7500  oaordex  7598  dfac2  8913  zorn2lem4  9281  zorn2lem7  9284  psslinpr  9813  facwordi  13032  ndvdssub  15076  pmtrfrn  17818  elcls  20817  elcls3  20827  neibl  22246  met2ndc  22268  itgcn  23549  branmfn  28852  atcvatlem  29132  atcvat4i  29144  prtlem15  33679  cvlsupr4  34151  cvlsupr5  34152  cvlsupr6  34153  2llnneN  34214  cvrat4  34248  llnexchb2  34674  cdleme48gfv1  35343  cdlemg6e  35429  dihord6apre  36064  dihord5b  36067  dihord5apre  36070  dihglblem5apreN  36099  dihglbcpreN  36108
 Copyright terms: Public domain W3C validator