Theorem exp4a 436

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

Syntax hints:   → wi 4   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  exp4d  438  exp45  443  exp5c  449  tz7.7  6388  tfr3  8387  oaass  8547  omordi  8552  nnmordi  8618  fiint  9287  zorn2lem6  10486  zorn2lem7  10487  mulgt0sr  11091  sqlecan  14247  rexuzre  15406  caurcvg  15730  ndvdssub  16468  lsmcv  21246  iscnp4  23401  nrmsep3  23493  2ndcdisj  23594  2ndcsep  23597  tsmsxp  24293  metcnp3  24678  xrlimcnp  27111  ax5seglem5  29261  elspansn4  31903  hoadddir  32134  atcvatlem  32715  sumdmdii  32745  sumdmdlem  32748  isbasisrelowllem1  37979  isbasisrelowllem2  37980  disjlem17  39529  prtlem17  39628  cvratlem  40173  athgt  40208  lplnnle2at  40293  lplncvrlvol2  40367  cdlemb  40546  dalaw  40638  cdleme50trn2  41303  cdlemg18b  41431  dihmeetlem3N  42057  onfrALTlem2  45235  in3an  45300  lindslinindsimp1  49214