Theorem exp4a 634

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

Syntax hints:   → wi 4   ∧ wa 383

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 197  df-an 385

This theorem is referenced by:  exp4bOLD  636  exp4d  638  exp45  643  exp5c  645  tz7.7  5910  wfrlem12  7595  tfr3  7664  oaass  7810  omordi  7815  nnmordi  7880  fiint  8402  zorn2lem6  9515  zorn2lem7  9516  mulgt0sr  10118  sqlecan  13165  rexuzre  14291  caurcvg  14606  ndvdssub  15335  lsmcv  19343  iscnp4  21269  nrmsep3  21361  2ndcdisj  21461  2ndcsep  21464  tsmsxp  22159  metcnp3  22546  xrlimcnp  24894  ax5seglem5  26012  elspansn4  28741  hoadddir  28972  atcvatlem  29553  sumdmdii  29583  sumdmdlem  29586  isbasisrelowllem1  33514  isbasisrelowllem2  33515  prtlem17  34665  cvratlem  35210  athgt  35245  lplnnle2at  35330  lplncvrlvol2  35404  cdlemb  35583  dalaw  35675  cdleme50trn2  36341  cdlemg18b  36469  dihmeetlem3N  37096  onfrALTlem2  39263  in3an  39338  lindslinindsimp1  42756