Theorem exp4a 435

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

Syntax hints:   → wi 4   ∧ wa 399

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 209  df-an 400

This theorem is referenced by:  exp4d  437  exp45  442  exp5c  448  tz7.7  6368  tfr3  8365  oaass  8525  omordi  8530  nnmordi  8596  fiint  9267  zorn2lem6  10455  zorn2lem7  10456  mulgt0sr  11060  sqlecan  14219  rexuzre  15363  caurcvg  15687  ndvdssub  16426  lsmcv  21191  iscnp4  23303  nrmsep3  23395  2ndcdisj  23496  2ndcsep  23499  tsmsxp  24195  metcnp3  24580  xrlimcnp  27010  ax5seglem5  29080  elspansn4  31722  hoadddir  31953  atcvatlem  32534  sumdmdii  32564  sumdmdlem  32567  isbasisrelowllem1  37813  isbasisrelowllem2  37814  disjlem17  39365  prtlem17  39464  cvratlem  40009  athgt  40044  lplnnle2at  40129  lplncvrlvol2  40203  cdlemb  40382  dalaw  40474  cdleme50trn2  41139  cdlemg18b  41267  dihmeetlem3N  41893  onfrALTlem2  45086  in3an  45151  lindslinindsimp1  49043