Theorem exp4a 431

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

Syntax hints:   → wi 4   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  exp4d  433  exp45  438  exp5c  444  tz7.7  6412  wfrlem12OLD  8359  tfr3  8438  oaass  8598  omordi  8603  nnmordi  8668  fiint  9364  fiintOLD  9365  zorn2lem6  10539  zorn2lem7  10540  mulgt0sr  11143  sqlecan  14245  rexuzre  15388  caurcvg  15710  ndvdssub  16443  lsmcv  21161  iscnp4  23287  nrmsep3  23379  2ndcdisj  23480  2ndcsep  23483  tsmsxp  24179  metcnp3  24569  xrlimcnp  27026  ax5seglem5  28963  elspansn4  31602  hoadddir  31833  atcvatlem  32414  sumdmdii  32444  sumdmdlem  32447  isbasisrelowllem1  37338  isbasisrelowllem2  37339  disjlem17  38781  prtlem17  38858  cvratlem  39404  athgt  39439  lplnnle2at  39524  lplncvrlvol2  39598  cdlemb  39777  dalaw  39869  cdleme50trn2  40534  cdlemg18b  40662  dihmeetlem3N  41288  onfrALTlem2  44544  in3an  44609  lindslinindsimp1  48303