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

Theorem exp4a 418
Description: An exportation inference. (Contributed by NM, 26-Apr-1994.) (Proof shortened by Wolf Lammen, 20-Jul-2021.)
Hypothesis
Ref Expression
exp4a.1 (𝜑 → (𝜓 → ((𝜒𝜃) → 𝜏)))
Assertion
Ref Expression
exp4a (𝜑 → (𝜓 → (𝜒 → (𝜃𝜏))))

Proof of Theorem exp4a
StepHypRef Expression
1 exp4a.1 . . 3 (𝜑 → (𝜓 → ((𝜒𝜃) → 𝜏)))
21imp 393 . 2 ((𝜑𝜓) → ((𝜒𝜃) → 𝜏))
32exp4b 417 1 (𝜑 → (𝜓 → (𝜒 → (𝜃𝜏))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382
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 383
This theorem is referenced by:  exp4d  420  exp45  425  exp5c  431  tz7.7  5892  wfrlem12  7578  tfr3  7647  oaass  7794  omordi  7799  nnmordi  7864  fiint  8392  zorn2lem6  9524  zorn2lem7  9525  mulgt0sr  10127  sqlecan  13177  rexuzre  14299  caurcvg  14614  ndvdssub  15340  lsmcv  19354  iscnp4  21287  nrmsep3  21379  2ndcdisj  21479  2ndcsep  21482  tsmsxp  22177  metcnp3  22564  xrlimcnp  24915  ax5seglem5  26033  elspansn4  28766  hoadddir  28997  atcvatlem  29578  sumdmdii  29608  sumdmdlem  29611  isbasisrelowllem1  33533  isbasisrelowllem2  33534  prtlem17  34677  cvratlem  35222  athgt  35257  lplnnle2at  35342  lplncvrlvol2  35416  cdlemb  35595  dalaw  35687  cdleme50trn2  36353  cdlemg18b  36481  dihmeetlem3N  37108  onfrALTlem2  39280  in3an  39355  lindslinindsimp1  42764
  Copyright terms: Public domain W3C validator