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  6341  tfr3  8329  oaass  8487  omordi  8492  nnmordi  8558  fiint  9228  zorn2lem6  10412  zorn2lem7  10413  mulgt0sr  11017  sqlecan  14160  rexuzre  15304  caurcvg  15628  ndvdssub  16367  lsmcv  21129  iscnp4  23237  nrmsep3  23329  2ndcdisj  23430  2ndcsep  23433  tsmsxp  24129  metcnp3  24514  xrlimcnp  26949  ax5seglem5  29021  elspansn4  31664  hoadddir  31895  atcvatlem  32476  sumdmdii  32506  sumdmdlem  32509  isbasisrelowllem1  37682  isbasisrelowllem2  37683  disjlem17  39234  prtlem17  39333  cvratlem  39878  athgt  39913  lplnnle2at  39998  lplncvrlvol2  40072  cdlemb  40251  dalaw  40343  cdleme50trn2  41008  cdlemg18b  41136  dihmeetlem3N  41762  onfrALTlem2  44988  in3an  45053  lindslinindsimp1  48930