Theorem exp4a 434

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

Syntax hints:   → wi 4   ∧ wa 398

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 399

This theorem is referenced by:  exp4d  436  exp45  441  exp5c  447  tz7.7  6220  wfrlem12  7969  tfr3  8038  oaass  8190  omordi  8195  nnmordi  8260  fiint  8798  zorn2lem6  9926  zorn2lem7  9927  mulgt0sr  10530  sqlecan  13574  rexuzre  14715  caurcvg  15036  ndvdssub  15763  lsmcv  19916  iscnp4  21874  nrmsep3  21966  2ndcdisj  22067  2ndcsep  22070  tsmsxp  22766  metcnp3  23153  xrlimcnp  25549  ax5seglem5  26722  elspansn4  29353  hoadddir  29584  atcvatlem  30165  sumdmdii  30195  sumdmdlem  30198  isbasisrelowllem1  34640  isbasisrelowllem2  34641  prtlem17  36016  cvratlem  36561  athgt  36596  lplnnle2at  36681  lplncvrlvol2  36755  cdlemb  36934  dalaw  37026  cdleme50trn2  37691  cdlemg18b  37819  dihmeetlem3N  38445  onfrALTlem2  40886  in3an  40951  lindslinindsimp1  44519