Theorem exp4a 437

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 412	. 2 ⊢ ((𝜑 ∧ 𝜓) → ((𝜒 ∧ 𝜃) → 𝜏))
3	2	exp4b 436	1 ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏))))

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  exp4d  439  exp45  444  exp5c  450  tz7.7  6389  tfr3  8408  oaass  8570  omordi  8575  nnmordi  8641  fiint  9319  zorn2lem6  10580  zorn2lem7  10581  mulgt0sr  11191  sqlecan  14354  rexuzre  15521  caurcvg  15845  ndvdssub  16580  lsmcv  21420  iscnp4  23582  nrmsep3  23674  2ndcdisj  23776  2ndcsep  23779  tsmsxp  24475  metcnp3  24860  xrlimcnp  27297  ax5seglem5  29512  elspansn4  32176  hoadddir  32407  atcvatlem  32988  sumdmdii  33018  sumdmdlem  33021  isbasisrelowllem1  38280  isbasisrelowllem2  38281  disjlem17  39836  prtlem17  39935  cvratlem  40480  athgt  40515  lplnnle2at  40600  lplncvrlvol2  40674  cdlemb  40853  dalaw  40945  cdleme50trn2  41610  cdlemg18b  41738  dihmeetlem3N  42364  onfrALTlem2  45530  in3an  45595  lindslinindsimp1  49570