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 206  df-an 396

This theorem is referenced by:  exp4d  433  exp45  438  exp5c  444  tz7.7  6277  wfrlem12OLD  8122  tfr3  8201  oaass  8354  omordi  8359  nnmordi  8424  fiint  9021  zorn2lem6  10188  zorn2lem7  10189  mulgt0sr  10792  sqlecan  13853  rexuzre  14992  caurcvg  15316  ndvdssub  16046  lsmcv  20318  iscnp4  22322  nrmsep3  22414  2ndcdisj  22515  2ndcsep  22518  tsmsxp  23214  metcnp3  23602  xrlimcnp  26023  ax5seglem5  27204  elspansn4  29836  hoadddir  30067  atcvatlem  30648  sumdmdii  30678  sumdmdlem  30681  isbasisrelowllem1  35453  isbasisrelowllem2  35454  prtlem17  36817  cvratlem  37362  athgt  37397  lplnnle2at  37482  lplncvrlvol2  37556  cdlemb  37735  dalaw  37827  cdleme50trn2  38492  cdlemg18b  38620  dihmeetlem3N  39246  onfrALTlem2  42055  in3an  42120  lindslinindsimp1  45686