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  6337  tfr3  8324  oaass  8482  omordi  8487  nnmordi  8552  fiint  9218  zorn2lem6  10399  zorn2lem7  10400  mulgt0sr  11003  sqlecan  14118  rexuzre  15262  caurcvg  15586  ndvdssub  16322  lsmcv  21080  iscnp4  23179  nrmsep3  23271  2ndcdisj  23372  2ndcsep  23375  tsmsxp  24071  metcnp3  24456  xrlimcnp  26906  ax5seglem5  28913  elspansn4  31555  hoadddir  31786  atcvatlem  32367  sumdmdii  32397  sumdmdlem  32400  isbasisrelowllem1  37420  isbasisrelowllem2  37421  disjlem17  38917  prtlem17  38995  cvratlem  39540  athgt  39575  lplnnle2at  39660  lplncvrlvol2  39734  cdlemb  39913  dalaw  40005  cdleme50trn2  40670  cdlemg18b  40798  dihmeetlem3N  41424  onfrALTlem2  44663  in3an  44728  lindslinindsimp1  48582