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  6388  tfr3  8410  oaass  8572  omordi  8577  nnmordi  8643  fiint  9321  zorn2lem6  10582  zorn2lem7  10583  mulgt0sr  11193  sqlecan  14356  rexuzre  15525  caurcvg  15849  ndvdssub  16584  lsmcv  21424  iscnp4  23586  nrmsep3  23678  2ndcdisj  23780  2ndcsep  23783  tsmsxp  24479  metcnp3  24864  xrlimcnp  27301  ax5seglem5  29516  elspansn4  32180  hoadddir  32411  atcvatlem  32992  sumdmdii  33022  sumdmdlem  33025  isbasisrelowllem1  38371  isbasisrelowllem2  38372  disjlem17  39927  prtlem17  40026  cvratlem  40571  athgt  40606  lplnnle2at  40691  lplncvrlvol2  40765  cdlemb  40944  dalaw  41036  cdleme50trn2  41701  cdlemg18b  41829  dihmeetlem3N  42455  onfrALTlem2  45622  in3an  45687  lindslinindsimp1  49662