Theorem exp4a 432

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

Syntax hints:   → wi 4   ∧ wa 396

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 208  df-an 397

This theorem is referenced by:  exp4d  434  exp45  439  exp5c  445  tz7.7  6097  wfrlem12  7823  tfr3  7892  oaass  8042  omordi  8047  nnmordi  8112  fiint  8646  zorn2lem6  9774  zorn2lem7  9775  mulgt0sr  10378  sqlecan  13426  rexuzre  14551  caurcvg  14872  ndvdssub  15598  lsmcv  19608  iscnp4  21560  nrmsep3  21652  2ndcdisj  21753  2ndcsep  21756  tsmsxp  22451  metcnp3  22838  xrlimcnp  25233  ax5seglem5  26407  elspansn4  29046  hoadddir  29277  atcvatlem  29858  sumdmdii  29888  sumdmdlem  29891  isbasisrelowllem1  34192  isbasisrelowllem2  34193  prtlem17  35568  cvratlem  36113  athgt  36148  lplnnle2at  36233  lplncvrlvol2  36307  cdlemb  36486  dalaw  36578  cdleme50trn2  37243  cdlemg18b  37371  dihmeetlem3N  37997  onfrALTlem2  40444  in3an  40509  lindslinindsimp1  44018