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  6351  tfr3  8340  oaass  8498  omordi  8503  nnmordi  8569  fiint  9239  zorn2lem6  10423  zorn2lem7  10424  mulgt0sr  11028  sqlecan  14144  rexuzre  15288  caurcvg  15612  ndvdssub  16348  lsmcv  21108  iscnp4  23219  nrmsep3  23311  2ndcdisj  23412  2ndcsep  23415  tsmsxp  24111  metcnp3  24496  xrlimcnp  26946  ax5seglem5  29018  elspansn4  31660  hoadddir  31891  atcvatlem  32472  sumdmdii  32502  sumdmdlem  32505  isbasisrelowllem1  37604  isbasisrelowllem2  37605  disjlem17  39147  prtlem17  39246  cvratlem  39791  athgt  39826  lplnnle2at  39911  lplncvrlvol2  39985  cdlemb  40164  dalaw  40256  cdleme50trn2  40921  cdlemg18b  41049  dihmeetlem3N  41675  onfrALTlem2  44896  in3an  44961  lindslinindsimp1  48811