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

This theorem is referenced by:  exp4d  437  exp45  442  exp5c  448  tz7.7  6239  wfrlem12  8066  tfr3  8135  oaass  8289  omordi  8294  nnmordi  8359  fiint  8948  zorn2lem6  10115  zorn2lem7  10116  mulgt0sr  10719  sqlecan  13777  rexuzre  14916  caurcvg  15240  ndvdssub  15970  lsmcv  20178  iscnp4  22160  nrmsep3  22252  2ndcdisj  22353  2ndcsep  22356  tsmsxp  23052  metcnp3  23438  xrlimcnp  25851  ax5seglem5  27024  elspansn4  29654  hoadddir  29885  atcvatlem  30466  sumdmdii  30496  sumdmdlem  30499  isbasisrelowllem1  35263  isbasisrelowllem2  35264  prtlem17  36627  cvratlem  37172  athgt  37207  lplnnle2at  37292  lplncvrlvol2  37366  cdlemb  37545  dalaw  37637  cdleme50trn2  38302  cdlemg18b  38430  dihmeetlem3N  39056  onfrALTlem2  41839  in3an  41904  lindslinindsimp1  45471