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  6376  tfr3  8374  oaass  8534  omordi  8539  nnmordi  8605  fiint  9274  zorn2lem6  10473  zorn2lem7  10474  mulgt0sr  11078  sqlecan  14236  rexuzre  15394  caurcvg  15718  ndvdssub  16457  lsmcv  21234  iscnp4  23381  nrmsep3  23473  2ndcdisj  23574  2ndcsep  23577  tsmsxp  24273  metcnp3  24658  xrlimcnp  27091  ax5seglem5  29192  elspansn4  31834  hoadddir  32065  atcvatlem  32646  sumdmdii  32676  sumdmdlem  32679  isbasisrelowllem1  37861  isbasisrelowllem2  37862  disjlem17  39413  prtlem17  39512  cvratlem  40057  athgt  40092  lplnnle2at  40177  lplncvrlvol2  40251  cdlemb  40430  dalaw  40522  cdleme50trn2  41187  cdlemg18b  41315  dihmeetlem3N  41941  onfrALTlem2  45120  in3an  45185  lindslinindsimp1  49088