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  6381  tfr3  8391  oaass  8553  omordi  8558  nnmordi  8624  fiint  9302  zorn2lem6  10560  zorn2lem7  10561  mulgt0sr  11171  sqlecan  14333  rexuzre  15500  caurcvg  15824  ndvdssub  16559  lsmcv  21399  iscnp4  23561  nrmsep3  23653  2ndcdisj  23755  2ndcsep  23758  tsmsxp  24454  metcnp3  24839  xrlimcnp  27278  ax5seglem5  29493  elspansn4  32157  hoadddir  32388  atcvatlem  32969  sumdmdii  32999  sumdmdlem  33002  isbasisrelowllem1  38246  isbasisrelowllem2  38247  disjlem17  39802  prtlem17  39901  cvratlem  40446  athgt  40481  lplnnle2at  40566  lplncvrlvol2  40640  cdlemb  40819  dalaw  40911  cdleme50trn2  41576  cdlemg18b  41704  dihmeetlem3N  42330  onfrALTlem2  45488  in3an  45553  lindslinindsimp1  49513