Theorem exp4b 421

Description: An exportation inference. (Contributed by NM, 26-Apr-1994.) (Proof shortened by Wolf Lammen, 23-Nov-2012.) Shorten exp4a 422. (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 404	. 2 ⊢ ((𝜑 ∧ 𝜓) → (𝜒 → (𝜃 → 𝜏)))
3	2	ex 401	1 ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏))))

Syntax hints:   → wi 4   ∧ wa 384

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 198  df-an 385

This theorem is referenced by:  exp4a  422  exp43  427  somo  5232  tz7.7  5934  f1oweALT  7350  onfununi  7642  odi  7864  omeu  7870  nndi  7908  inf3lem2  8741  axdc3lem2  9526  genpnmax  10082  mulclprlem  10094  distrlem5pr  10102  reclem4pr  10125  lemul12a  11135  sup2  11233  nnmulcl  11299  nnmulclOLD  11300  zbtwnre  11987  elfz0fzfz0  12652  fzofzim  12723  fzo1fzo0n0  12727  elincfzoext  12734  elfzodifsumelfzo  12742  le2sq2  13146  expnbnd  13200  swrdswrd  13692  swrdccat3blem  13749  climbdd  14689  dvdslegcd  15509  oddprmgt2  15693  unbenlem  15893  infpnlem1  15895  prmgaplem6  16041  lmodvsdi  19155  lspsolvlem  19415  lbsextlem2  19433  gsummoncoe1  19947  cpmatmcllem  20802  mp2pm2mplem4  20893  1stccnp  21545  itg2le  23797  ewlkle  26792  clwlkclwwlklem2a  27204  3vfriswmgr  27516  frgrwopreg  27561  frgr2wwlk1  27567  frgrreg  27645  spansneleq  28820  elspansn4  28823  cvmdi  29574  atcvat3i  29646  mdsymlem3  29655  slmdvsdi  30150  mclsppslem  31860  dfon2lem8  32070  soseq  32130  heicant  33800  areacirclem1  33855  areacirclem2  33856  areacirclem4  33858  areacirc  33860  fzmul  33891  cvlexch1  35216  hlrelat2  35291  cvrat3  35330  snatpsubN  35638  pmaple  35649  fzopredsuc  41999  gbegt5  42257