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  6393  tfr3  8395  oaass  8555  omordi  8560  nnmordi  8626  fiint  9296  zorn2lem6  10503  zorn2lem7  10504  mulgt0sr  11108  sqlecan  14265  rexuzre  15430  caurcvg  15754  ndvdssub  16492  lsmcv  21302  iscnp4  23457  nrmsep3  23549  2ndcdisj  23650  2ndcsep  23653  tsmsxp  24349  metcnp3  24734  xrlimcnp  27170  ax5seglem5  29320  elspansn4  31962  hoadddir  32193  atcvatlem  32774  sumdmdii  32804  sumdmdlem  32807  isbasisrelowllem1  38042  isbasisrelowllem2  38043  disjlem17  39592  prtlem17  39691  cvratlem  40236  athgt  40271  lplnnle2at  40356  lplncvrlvol2  40430  cdlemb  40609  dalaw  40701  cdleme50trn2  41366  cdlemg18b  41494  dihmeetlem3N  42120  onfrALTlem2  45296  in3an  45361  lindslinindsimp1  49278