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

Theorem exp4a 435
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 410 . 2 ((𝜑𝜓) → ((𝜒𝜃) → 𝜏))
32exp4b 434 1 (𝜑 → (𝜓 → (𝜒 → (𝜃𝜏))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399
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 210  df-an 400
This theorem is referenced by:  exp4d  437  exp45  442  exp5c  448  tz7.7  6239  wfrlem12  8066  tfr3  8135  oaass  8289  omordi  8294  nnmordi  8359  fiint  8948  zorn2lem6  10115  zorn2lem7  10116  mulgt0sr  10719  sqlecan  13777  rexuzre  14916  caurcvg  15240  ndvdssub  15970  lsmcv  20178  iscnp4  22160  nrmsep3  22252  2ndcdisj  22353  2ndcsep  22356  tsmsxp  23052  metcnp3  23438  xrlimcnp  25851  ax5seglem5  27024  elspansn4  29654  hoadddir  29885  atcvatlem  30466  sumdmdii  30496  sumdmdlem  30499  isbasisrelowllem1  35263  isbasisrelowllem2  35264  prtlem17  36627  cvratlem  37172  athgt  37207  lplnnle2at  37292  lplncvrlvol2  37366  cdlemb  37545  dalaw  37637  cdleme50trn2  38302  cdlemg18b  38430  dihmeetlem3N  39056  onfrALTlem2  41839  in3an  41904  lindslinindsimp1  45471
  Copyright terms: Public domain W3C validator