Theorem exp4a 437

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  exp4d  439  exp45  444  exp5c  450  tz7.7  6406  tfr3  8435  oaass  8597  omordi  8602  nnmordi  8668  fiint  9346  zorn2lem6  10606  zorn2lem7  10607  mulgt0sr  11217  sqlecan  14380  rexuzre  15549  caurcvg  15873  ndvdssub  16608  lsmcv  21449  iscnp4  23611  nrmsep3  23703  2ndcdisj  23805  2ndcsep  23808  tsmsxp  24504  metcnp3  24889  xrlimcnp  27326  ax5seglem5  29541  elspansn4  32205  hoadddir  32436  atcvatlem  33017  sumdmdii  33047  sumdmdlem  33050  isbasisrelowllem1  38470  isbasisrelowllem2  38471  disjlem17  40026  prtlem17  40125  cvratlem  40670  athgt  40705  lplnnle2at  40790  lplncvrlvol2  40864  cdlemb  41043  dalaw  41135  cdleme50trn2  41800  cdlemg18b  41928  dihmeetlem3N  42554  onfrALTlem2  45720  in3an  45785  lindslinindsimp1  49774