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  6343  tfr3  8330  oaass  8488  omordi  8493  nnmordi  8559  fiint  9227  zorn2lem6  10411  zorn2lem7  10412  mulgt0sr  11016  sqlecan  14132  rexuzre  15276  caurcvg  15600  ndvdssub  16336  lsmcv  21096  iscnp4  23207  nrmsep3  23299  2ndcdisj  23400  2ndcsep  23403  tsmsxp  24099  metcnp3  24484  xrlimcnp  26934  ax5seglem5  29006  elspansn4  31648  hoadddir  31879  atcvatlem  32460  sumdmdii  32490  sumdmdlem  32493  isbasisrelowllem1  37556  isbasisrelowllem2  37557  disjlem17  39054  prtlem17  39132  cvratlem  39677  athgt  39712  lplnnle2at  39797  lplncvrlvol2  39871  cdlemb  40050  dalaw  40142  cdleme50trn2  40807  cdlemg18b  40935  dihmeetlem3N  41561  onfrALTlem2  44783  in3an  44848  lindslinindsimp1  48699