Theorem exp4b 429

Description: An exportation inference. (Contributed by NM, 26-Apr-1994.) (Proof shortened by Wolf Lammen, 23-Nov-2012.) Shorten exp4a 430. (Revised by Wolf Lammen, 20-Jul-2021.)

Hypothesis

Ref	Expression
exp4b.1	⊢ ((𝜑 ∧ 𝜓) → ((𝜒 ∧ 𝜃) → 𝜏))

Assertion

Ref	Expression
exp4b	⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏))))

Proof of Theorem exp4b

Step	Hyp	Ref	Expression
1		exp4b.1	. . 3 ⊢ ((𝜑 ∧ 𝜓) → ((𝜒 ∧ 𝜃) → 𝜏))
2	1	expd 414	. 2 ⊢ ((𝜑 ∧ 𝜓) → (𝜒 → (𝜃 → 𝜏)))
3	2	ex 411	1 ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏))))

Syntax hints:   → wi 4   ∧ wa 394

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 395

This theorem is referenced by:  exp4a  430  exp43  435  somo  5627  tz7.7  6397  f1oweALT  7977  soseq  8164  onfununi  8362  odi  8600  omeu  8606  nndi  8644  inf3lem2  9659  axdc3lem2  10481  genpnmax  11037  mulclprlem  11049  distrlem5pr  11057  reclem4pr  11080  lemul12a  12110  sup2  12208  nnmulcl  12274  zbtwnre  12968  elfz0fzfz0  13646  fzofzim  13719  fzo1fzo0n0  13723  elincfzoext  13730  elfzodifsumelfzo  13738  le2sq2  14140  expnbnd  14235  swrdswrd  14696  swrdccat3blem  14730  climbdd  15659  dvdslegcd  16487  oddprmgt2  16678  unbenlem  16885  infpnlem1  16887  prmgaplem6  17033  lmodvsdi  20785  lspsolvlem  21047  lbsextlem2  21064  gsummoncoe1  22257  cpmatmcllem  22669  mp2pm2mplem4  22760  1stccnp  23415  itg2le  25718  ewlkle  29496  clwlkclwwlklem2a  29885  3vfriswmgr  30165  frgrwopreg  30210  frgr2wwlk1  30216  frgrreg  30281  spansneleq  31457  elspansn4  31460  cvmdi  32211  atcvat3i  32283  mdsymlem3  32292  slmdvsdi  33019  satfv0  35101  satffunlem1lem1  35145  satffunlem2lem1  35147  mclsppslem  35326  dfon2lem8  35519  heicant  37261  areacirclem1  37314  areacirclem2  37315  areacirclem4  37317  areacirc  37319  fzmul  37347  cvlexch1  38932  hlrelat2  39008  cvrat3  39047  snatpsubN  39355  pmaple  39366  sn-sup2  42161  fzopredsuc  46843  gbegt5  47240