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  6383  wfrlem12OLD  8339  tfr3  8418  oaass  8578  omordi  8583  nnmordi  8648  fiint  9343  fiintOLD  9344  zorn2lem6  10520  zorn2lem7  10521  mulgt0sr  11124  sqlecan  14232  rexuzre  15376  caurcvg  15698  ndvdssub  16433  lsmcv  21107  iscnp4  23206  nrmsep3  23298  2ndcdisj  23399  2ndcsep  23402  tsmsxp  24098  metcnp3  24484  xrlimcnp  26935  ax5seglem5  28917  elspansn4  31559  hoadddir  31790  atcvatlem  32371  sumdmdii  32401  sumdmdlem  32404  isbasisrelowllem1  37378  isbasisrelowllem2  37379  disjlem17  38822  prtlem17  38899  cvratlem  39445  athgt  39480  lplnnle2at  39565  lplncvrlvol2  39639  cdlemb  39818  dalaw  39910  cdleme50trn2  40575  cdlemg18b  40703  dihmeetlem3N  41329  onfrALTlem2  44538  in3an  44603  lindslinindsimp1  48400