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

Theorem imp4a 615
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 614 . 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 197  df-an 385
This theorem is referenced by:  imp4bOLD  617  imp4d  619  imp55  628  imp511  629  reuss2  4050  wefrc  5260  f1oweALT  7318  tfrlem9  7651  tz7.49  7710  oaordex  7809  dfac2b  9163  dfac2OLD  9165  zorn2lem4  9533  zorn2lem7  9536  psslinpr  10065  facwordi  13290  ndvdssub  15355  pmtrfrn  18098  elcls  21099  elcls3  21109  neibl  22527  met2ndc  22549  itgcn  23828  branmfn  29294  atcvatlem  29574  atcvat4i  29586  prtlem15  34682  cvlsupr4  35153  cvlsupr5  35154  cvlsupr6  35155  2llnneN  35216  cvrat4  35250  llnexchb2  35676  cdleme48gfv1  36344  cdlemg6e  36430  dihord6apre  37065  dihord5b  37068  dihord5apre  37071  dihglblem5apreN  37100  dihglbcpreN  37109
  Copyright terms: Public domain W3C validator