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

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

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 206  df-an 397

This theorem is referenced by:  exp4d  434  exp45  439  exp5c  445  tz7.7  6292  wfrlem12OLD  8151  tfr3  8230  oaass  8392  omordi  8397  nnmordi  8462  fiint  9091  zorn2lem6  10257  zorn2lem7  10258  mulgt0sr  10861  sqlecan  13925  rexuzre  15064  caurcvg  15388  ndvdssub  16118  lsmcv  20403  iscnp4  22414  nrmsep3  22506  2ndcdisj  22607  2ndcsep  22610  tsmsxp  23306  metcnp3  23696  xrlimcnp  26118  ax5seglem5  27301  elspansn4  29935  hoadddir  30166  atcvatlem  30747  sumdmdii  30777  sumdmdlem  30780  isbasisrelowllem1  35526  isbasisrelowllem2  35527  prtlem17  36890  cvratlem  37435  athgt  37470  lplnnle2at  37555  lplncvrlvol2  37629  cdlemb  37808  dalaw  37900  cdleme50trn2  38565  cdlemg18b  38693  dihmeetlem3N  39319  onfrALTlem2  42166  in3an  42231  lindslinindsimp1  45798