Theorem exp4a 431

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

Syntax hints:   → wi 4   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  exp4d  433  exp45  438  exp5c  444  tz7.7  6361  tfr3  8370  oaass  8528  omordi  8533  nnmordi  8598  fiint  9284  fiintOLD  9285  zorn2lem6  10461  zorn2lem7  10462  mulgt0sr  11065  sqlecan  14181  rexuzre  15326  caurcvg  15650  ndvdssub  16386  lsmcv  21058  iscnp4  23157  nrmsep3  23249  2ndcdisj  23350  2ndcsep  23353  tsmsxp  24049  metcnp3  24435  xrlimcnp  26885  ax5seglem5  28867  elspansn4  31509  hoadddir  31740  atcvatlem  32321  sumdmdii  32351  sumdmdlem  32354  isbasisrelowllem1  37350  isbasisrelowllem2  37351  disjlem17  38798  prtlem17  38876  cvratlem  39422  athgt  39457  lplnnle2at  39542  lplncvrlvol2  39616  cdlemb  39795  dalaw  39887  cdleme50trn2  40552  cdlemg18b  40680  dihmeetlem3N  41306  onfrALTlem2  44543  in3an  44608  lindslinindsimp1  48450