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  6409  wfrlem12OLD  8361  tfr3  8440  oaass  8600  omordi  8605  nnmordi  8670  fiint  9367  fiintOLD  9368  zorn2lem6  10542  zorn2lem7  10543  mulgt0sr  11146  sqlecan  14249  rexuzre  15392  caurcvg  15714  ndvdssub  16447  lsmcv  21144  iscnp4  23272  nrmsep3  23364  2ndcdisj  23465  2ndcsep  23468  tsmsxp  24164  metcnp3  24554  xrlimcnp  27012  ax5seglem5  28949  elspansn4  31593  hoadddir  31824  atcvatlem  32405  sumdmdii  32435  sumdmdlem  32438  isbasisrelowllem1  37357  isbasisrelowllem2  37358  disjlem17  38801  prtlem17  38878  cvratlem  39424  athgt  39459  lplnnle2at  39544  lplncvrlvol2  39618  cdlemb  39797  dalaw  39889  cdleme50trn2  40554  cdlemg18b  40682  dihmeetlem3N  41308  onfrALTlem2  44571  in3an  44636  lindslinindsimp1  48379