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  6358  tfr3  8367  oaass  8525  omordi  8530  nnmordi  8595  fiint  9277  fiintOLD  9278  zorn2lem6  10454  zorn2lem7  10455  mulgt0sr  11058  sqlecan  14174  rexuzre  15319  caurcvg  15643  ndvdssub  16379  lsmcv  21051  iscnp4  23150  nrmsep3  23242  2ndcdisj  23343  2ndcsep  23346  tsmsxp  24042  metcnp3  24428  xrlimcnp  26878  ax5seglem5  28860  elspansn4  31502  hoadddir  31733  atcvatlem  32314  sumdmdii  32344  sumdmdlem  32347  isbasisrelowllem1  37343  isbasisrelowllem2  37344  disjlem17  38791  prtlem17  38869  cvratlem  39415  athgt  39450  lplnnle2at  39535  lplncvrlvol2  39609  cdlemb  39788  dalaw  39880  cdleme50trn2  40545  cdlemg18b  40673  dihmeetlem3N  41299  onfrALTlem2  44536  in3an  44601  lindslinindsimp1  48446