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  6421  wfrlem12OLD  8376  tfr3  8455  oaass  8617  omordi  8622  nnmordi  8687  fiint  9394  fiintOLD  9395  zorn2lem6  10570  zorn2lem7  10571  mulgt0sr  11174  sqlecan  14258  rexuzre  15401  caurcvg  15725  ndvdssub  16457  lsmcv  21166  iscnp4  23292  nrmsep3  23384  2ndcdisj  23485  2ndcsep  23488  tsmsxp  24184  metcnp3  24574  xrlimcnp  27029  ax5seglem5  28966  elspansn4  31605  hoadddir  31836  atcvatlem  32417  sumdmdii  32447  sumdmdlem  32450  isbasisrelowllem1  37321  isbasisrelowllem2  37322  disjlem17  38755  prtlem17  38832  cvratlem  39378  athgt  39413  lplnnle2at  39498  lplncvrlvol2  39572  cdlemb  39751  dalaw  39843  cdleme50trn2  40508  cdlemg18b  40636  dihmeetlem3N  41262  onfrALTlem2  44517  in3an  44582  lindslinindsimp1  48186