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  6349  tfr3  8338  oaass  8496  omordi  8501  nnmordi  8567  fiint  9237  zorn2lem6  10423  zorn2lem7  10424  mulgt0sr  11028  sqlecan  14171  rexuzre  15315  caurcvg  15639  ndvdssub  16378  lsmcv  21139  iscnp4  23228  nrmsep3  23320  2ndcdisj  23421  2ndcsep  23424  tsmsxp  24120  metcnp3  24505  xrlimcnp  26932  ax5seglem5  29002  elspansn4  31644  hoadddir  31875  atcvatlem  32456  sumdmdii  32486  sumdmdlem  32489  isbasisrelowllem1  37671  isbasisrelowllem2  37672  disjlem17  39223  prtlem17  39322  cvratlem  39867  athgt  39902  lplnnle2at  39987  lplncvrlvol2  40061  cdlemb  40240  dalaw  40332  cdleme50trn2  40997  cdlemg18b  41125  dihmeetlem3N  41751  onfrALTlem2  44973  in3an  45038  lindslinindsimp1  48933