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

Theorem exp4a 634
 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 444 . 2 ((𝜑𝜓) → ((𝜒𝜃) → 𝜏))
32exp4b 633 1 (𝜑 → (𝜓 → (𝜒 → (𝜃𝜏))))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 383 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 385 This theorem is referenced by:  exp4bOLD  636  exp4d  638  exp45  643  exp5c  645  tz7.7  5910  wfrlem12  7595  tfr3  7664  oaass  7810  omordi  7815  nnmordi  7880  fiint  8402  zorn2lem6  9515  zorn2lem7  9516  mulgt0sr  10118  sqlecan  13165  rexuzre  14291  caurcvg  14606  ndvdssub  15335  lsmcv  19343  iscnp4  21269  nrmsep3  21361  2ndcdisj  21461  2ndcsep  21464  tsmsxp  22159  metcnp3  22546  xrlimcnp  24894  ax5seglem5  26012  elspansn4  28741  hoadddir  28972  atcvatlem  29553  sumdmdii  29583  sumdmdlem  29586  isbasisrelowllem1  33514  isbasisrelowllem2  33515  prtlem17  34665  cvratlem  35210  athgt  35245  lplnnle2at  35330  lplncvrlvol2  35404  cdlemb  35583  dalaw  35675  cdleme50trn2  36341  cdlemg18b  36469  dihmeetlem3N  37096  onfrALTlem2  39263  in3an  39338  lindslinindsimp1  42756
 Copyright terms: Public domain W3C validator