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  6343  tfr3  8331  oaass  8489  omordi  8494  nnmordi  8560  fiint  9230  zorn2lem6  10414  zorn2lem7  10415  mulgt0sr  11019  sqlecan  14162  rexuzre  15306  caurcvg  15630  ndvdssub  16369  lsmcv  21131  iscnp4  23238  nrmsep3  23330  2ndcdisj  23431  2ndcsep  23434  tsmsxp  24130  metcnp3  24515  xrlimcnp  26945  ax5seglem5  29016  elspansn4  31659  hoadddir  31890  atcvatlem  32471  sumdmdii  32501  sumdmdlem  32504  isbasisrelowllem1  37685  isbasisrelowllem2  37686  disjlem17  39237  prtlem17  39336  cvratlem  39881  athgt  39916  lplnnle2at  40001  lplncvrlvol2  40075  cdlemb  40254  dalaw  40346  cdleme50trn2  41011  cdlemg18b  41139  dihmeetlem3N  41765  onfrALTlem2  44991  in3an  45056  lindslinindsimp1  48945