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

Theorem exp4a 432
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 407 . 2 ((𝜑𝜓) → ((𝜒𝜃) → 𝜏))
32exp4b 431 1 (𝜑 → (𝜓 → (𝜒 → (𝜃𝜏))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396
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 208  df-an 397
This theorem is referenced by:  exp4d  434  exp45  439  exp5c  445  tz7.7  6210  wfrlem12  7955  tfr3  8024  oaass  8176  omordi  8181  nnmordi  8246  fiint  8783  zorn2lem6  9911  zorn2lem7  9912  mulgt0sr  10515  sqlecan  13559  rexuzre  14700  caurcvg  15021  ndvdssub  15748  lsmcv  19842  iscnp4  21799  nrmsep3  21891  2ndcdisj  21992  2ndcsep  21995  tsmsxp  22690  metcnp3  23077  xrlimcnp  25473  ax5seglem5  26646  elspansn4  29277  hoadddir  29508  atcvatlem  30089  sumdmdii  30119  sumdmdlem  30122  isbasisrelowllem1  34518  isbasisrelowllem2  34519  prtlem17  35892  cvratlem  36437  athgt  36472  lplnnle2at  36557  lplncvrlvol2  36631  cdlemb  36810  dalaw  36902  cdleme50trn2  37567  cdlemg18b  37695  dihmeetlem3N  38321  onfrALTlem2  40757  in3an  40822  lindslinindsimp1  44440
  Copyright terms: Public domain W3C validator