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

Theorem exp4a 633
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 445 . 2 ((𝜑𝜓) → ((𝜒𝜃) → 𝜏))
32exp4b 632 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:  exp4bOLD  635  exp4d  637  exp45  642  exp5c  644  tz7.7  5747  wfrlem12  7423  tfr3  7492  oaass  7638  omordi  7643  nnmordi  7708  fiint  8234  zorn2lem6  9320  zorn2lem7  9321  mulgt0sr  9923  sqlecan  12966  rexuzre  14086  caurcvg  14401  ndvdssub  15127  lsmcv  19135  iscnp4  21061  nrmsep3  21153  2ndcdisj  21253  2ndcsep  21256  tsmsxp  21952  metcnp3  22339  xrlimcnp  24689  ax5seglem5  25807  elspansn4  28416  hoadddir  28647  atcvatlem  29228  sumdmdii  29258  sumdmdlem  29261  frrlem11  31776  isbasisrelowllem1  33183  isbasisrelowllem2  33184  prtlem17  33987  cvratlem  34533  athgt  34568  lplnnle2at  34653  lplncvrlvol2  34727  cdlemb  34906  dalaw  34998  cdleme50trn2  35665  cdlemg18b  35793  dihmeetlem3N  36420  onfrALTlem2  38587  in3an  38662  lindslinindsimp1  42017
  Copyright terms: Public domain W3C validator