Theorem exp4a 432

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

Syntax hints:   → wi 4   ∧ wa 396

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 206  df-an 397

This theorem is referenced by:  exp4d  434  exp45  439  exp5c  445  tz7.7  6348  wfrlem12OLD  8271  tfr3  8350  oaass  8513  omordi  8518  nnmordi  8583  fiint  9275  zorn2lem6  10446  zorn2lem7  10447  mulgt0sr  11050  sqlecan  14123  rexuzre  15249  caurcvg  15573  ndvdssub  16302  lsmcv  20661  iscnp4  22651  nrmsep3  22743  2ndcdisj  22844  2ndcsep  22847  tsmsxp  23543  metcnp3  23933  xrlimcnp  26355  ax5seglem5  27945  elspansn4  30578  hoadddir  30809  atcvatlem  31390  sumdmdii  31420  sumdmdlem  31423  isbasisrelowllem1  35899  isbasisrelowllem2  35900  disjlem17  37334  prtlem17  37411  cvratlem  37957  athgt  37992  lplnnle2at  38077  lplncvrlvol2  38151  cdlemb  38330  dalaw  38422  cdleme50trn2  39087  cdlemg18b  39215  dihmeetlem3N  39841  onfrALTlem2  42950  in3an  43015  lindslinindsimp1  46658