Theorem exp4a 631

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 630	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 196  df-an 385

This theorem is referenced by:  exp4bOLD  633  exp4d  635  exp45  640  exp5c  642  tz7.7  5666  wfrlem12  7313  tfr3  7382  oaass  7528  omordi  7533  nnmordi  7598  fiint  8122  zorn2lem6  9206  zorn2lem7  9207  mulgt0sr  9805  sqlecan  12833  rexuzre  13940  caurcvg  14255  ndvdssub  14971  lsmcv  18962  iscnp4  20877  nrmsep3  20969  2ndcdisj  21069  2ndcsep  21072  tsmsxp  21768  metcnp3  22155  xrlimcnp  24495  ax5seglem5  25613  elspansn4  27816  hoadddir  28047  atcvatlem  28628  sumdmdii  28658  sumdmdlem  28661  frrlem11  31036  isbasisrelowllem1  32379  isbasisrelowllem2  32380  prtlem17  33179  cvratlem  33725  athgt  33760  lplnnle2at  33845  lplncvrlvol2  33919  cdlemb  34098  dalaw  34190  cdleme50trn2  34857  cdlemg18b  34985  dihmeetlem3N  35612  onfrALTlem2  37782  in3an  37857  lindslinindsimp1  42040