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

This theorem is referenced by:  exp4d  434  exp45  439  exp5c  445  tz7.7  6343  tfr3  8335  oaass  8493  omordi  8498  nnmordi  8564  fiint  9234  zorn2lem6  10421  zorn2lem7  10422  mulgt0sr  11026  sqlecan  14169  rexuzre  15313  caurcvg  15637  ndvdssub  16376  lsmcv  21141  iscnp4  23253  nrmsep3  23345  2ndcdisj  23446  2ndcsep  23449  tsmsxp  24145  metcnp3  24530  xrlimcnp  26957  ax5seglem5  29027  elspansn4  31669  hoadddir  31900  atcvatlem  32481  sumdmdii  32511  sumdmdlem  32514  isbasisrelowllem1  37724  isbasisrelowllem2  37725  disjlem17  39276  prtlem17  39375  cvratlem  39920  athgt  39955  lplnnle2at  40040  lplncvrlvol2  40114  cdlemb  40293  dalaw  40385  cdleme50trn2  41050  cdlemg18b  41178  dihmeetlem3N  41804  onfrALTlem2  44997  in3an  45062  lindslinindsimp1  48955