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  6379  wfrlem12OLD  8302  tfr3  8381  oaass  8544  omordi  8549  nnmordi  8614  fiint  9307  zorn2lem6  10478  zorn2lem7  10479  mulgt0sr  11082  sqlecan  14155  rexuzre  15281  caurcvg  15605  ndvdssub  16334  lsmcv  20703  iscnp4  22696  nrmsep3  22788  2ndcdisj  22889  2ndcsep  22892  tsmsxp  23588  metcnp3  23978  xrlimcnp  26400  ax5seglem5  28056  elspansn4  30689  hoadddir  30920  atcvatlem  31501  sumdmdii  31531  sumdmdlem  31534  isbasisrelowllem1  36040  isbasisrelowllem2  36041  disjlem17  37474  prtlem17  37551  cvratlem  38097  athgt  38132  lplnnle2at  38217  lplncvrlvol2  38291  cdlemb  38470  dalaw  38562  cdleme50trn2  39227  cdlemg18b  39355  dihmeetlem3N  39981  onfrALTlem2  43078  in3an  43143  lindslinindsimp1  46786