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  6387  tfr3  8392  oaass  8552  omordi  8557  nnmordi  8623  fiint  9300  zorn2lem6  10507  zorn2lem7  10508  mulgt0sr  11118  sqlecan  14277  rexuzre  15444  caurcvg  15768  ndvdssub  16505  lsmcv  21334  iscnp4  23494  nrmsep3  23586  2ndcdisj  23688  2ndcsep  23691  tsmsxp  24387  metcnp3  24772  xrlimcnp  27213  ax5seglem5  29398  elspansn4  32062  hoadddir  32293  atcvatlem  32874  sumdmdii  32904  sumdmdlem  32907  isbasisrelowllem1  38117  isbasisrelowllem2  38118  disjlem17  39658  prtlem17  39757  cvratlem  40302  athgt  40337  lplnnle2at  40422  lplncvrlvol2  40496  cdlemb  40675  dalaw  40767  cdleme50trn2  41432  cdlemg18b  41560  dihmeetlem3N  42186  onfrALTlem2  45377  in3an  45442  lindslinindsimp1  49395