Theorem exp4a 431

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

Step	Hyp	Ref	Expression
1		exp4a.1	. . 3 ⊢ (𝜑 → (𝜓 → ((𝜒 ∧ 𝜃) → 𝜏)))
2	1	imp 406	. 2 ⊢ ((𝜑 ∧ 𝜓) → ((𝜒 ∧ 𝜃) → 𝜏))
3	2	exp4b 430	1 ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏))))

Syntax hints:   → wi 4   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  exp4d  433  exp45  438  exp5c  444  tz7.7  6332  tfr3  8318  oaass  8476  omordi  8481  nnmordi  8546  fiint  9211  zorn2lem6  10389  zorn2lem7  10390  mulgt0sr  10993  sqlecan  14113  rexuzre  15257  caurcvg  15581  ndvdssub  16317  lsmcv  21076  iscnp4  23176  nrmsep3  23268  2ndcdisj  23369  2ndcsep  23372  tsmsxp  24068  metcnp3  24453  xrlimcnp  26903  ax5seglem5  28909  elspansn4  31548  hoadddir  31779  atcvatlem  32360  sumdmdii  32390  sumdmdlem  32393  isbasisrelowllem1  37388  isbasisrelowllem2  37389  disjlem17  38836  prtlem17  38914  cvratlem  39459  athgt  39494  lplnnle2at  39579  lplncvrlvol2  39653  cdlemb  39832  dalaw  39924  cdleme50trn2  40589  cdlemg18b  40717  dihmeetlem3N  41343  onfrALTlem2  44578  in3an  44643  lindslinindsimp1  48488