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  6337  tfr3  8328  oaass  8486  omordi  8491  nnmordi  8556  fiint  9235  fiintOLD  9236  zorn2lem6  10414  zorn2lem7  10415  mulgt0sr  11018  sqlecan  14134  rexuzre  15278  caurcvg  15602  ndvdssub  16338  lsmcv  21066  iscnp4  23166  nrmsep3  23258  2ndcdisj  23359  2ndcsep  23362  tsmsxp  24058  metcnp3  24444  xrlimcnp  26894  ax5seglem5  28896  elspansn4  31535  hoadddir  31766  atcvatlem  32347  sumdmdii  32377  sumdmdlem  32380  isbasisrelowllem1  37328  isbasisrelowllem2  37329  disjlem17  38776  prtlem17  38854  cvratlem  39400  athgt  39435  lplnnle2at  39520  lplncvrlvol2  39594  cdlemb  39773  dalaw  39865  cdleme50trn2  40530  cdlemg18b  40658  dihmeetlem3N  41284  onfrALTlem2  44520  in3an  44585  lindslinindsimp1  48443