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

Theorem exp4a 420
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 395 . 2 ((𝜑𝜓) → ((𝜒𝜃) → 𝜏))
32exp4b 419 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 198  df-an 385
This theorem is referenced by:  exp4d  422  exp45  427  exp5c  433  tz7.7  5956  wfrlem12  7656  tfr3  7725  oaass  7872  omordi  7877  nnmordi  7942  fiint  8470  zorn2lem6  9602  zorn2lem7  9603  mulgt0sr  10205  sqlecan  13188  rexuzre  14309  caurcvg  14624  ndvdssub  15346  lsmcv  19343  iscnp4  21275  nrmsep3  21367  2ndcdisj  21467  2ndcsep  21470  tsmsxp  22165  metcnp3  22552  xrlimcnp  24903  ax5seglem5  26021  elspansn4  28754  hoadddir  28985  atcvatlem  29566  sumdmdii  29596  sumdmdlem  29599  isbasisrelowllem1  33513  isbasisrelowllem2  33514  prtlem17  34649  cvratlem  35195  athgt  35230  lplnnle2at  35315  lplncvrlvol2  35389  cdlemb  35568  dalaw  35660  cdleme50trn2  36326  cdlemg18b  36454  dihmeetlem3N  37080  onfrALTlem2  39253  in3an  39328  lindslinindsimp1  42808
  Copyright terms: Public domain W3C validator