Theorem exp4a 433

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

Syntax hints:   → wi 4   ∧ wa 397

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 398

This theorem is referenced by:  exp4d  435  exp45  440  exp5c  446  tz7.7  6391  wfrlem12OLD  8320  tfr3  8399  oaass  8561  omordi  8566  nnmordi  8631  fiint  9324  zorn2lem6  10496  zorn2lem7  10497  mulgt0sr  11100  sqlecan  14173  rexuzre  15299  caurcvg  15623  ndvdssub  16352  lsmcv  20754  iscnp4  22767  nrmsep3  22859  2ndcdisj  22960  2ndcsep  22963  tsmsxp  23659  metcnp3  24049  xrlimcnp  26473  ax5seglem5  28191  elspansn4  30826  hoadddir  31057  atcvatlem  31638  sumdmdii  31668  sumdmdlem  31671  isbasisrelowllem1  36236  isbasisrelowllem2  36237  disjlem17  37669  prtlem17  37746  cvratlem  38292  athgt  38327  lplnnle2at  38412  lplncvrlvol2  38486  cdlemb  38665  dalaw  38757  cdleme50trn2  39422  cdlemg18b  39550  dihmeetlem3N  40176  onfrALTlem2  43307  in3an  43372  lindslinindsimp1  47138