Theorem exp4b 430

Description: An exportation inference. (Contributed by NM, 26-Apr-1994.) (Proof shortened by Wolf Lammen, 23-Nov-2012.) Shorten exp4a 431. (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 415	. 2 ⊢ ((𝜑 ∧ 𝜓) → (𝜒 → (𝜃 → 𝜏)))
3	2	ex 412	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:  exp4a  431  exp43  436  somo  5571  tz7.7  6343  f1oweALT  7916  soseq  8101  onfununi  8273  odi  8506  omeu  8512  nndi  8551  inf3lem2  9538  axdc3lem2  10361  genpnmax  10918  mulclprlem  10930  distrlem5pr  10938  reclem4pr  10961  lemul12a  11999  sup2  12098  nnmulcl  12169  zbtwnre  12859  elfz0fzfz0  13549  fzofzim  13625  fzo1fzo0n0  13631  elincfzoext  13639  elfzodifsumelfzo  13647  le2sq2  14058  expnbnd  14155  swrdswrd  14628  swrdccat3blem  14662  climbdd  15595  dvdslegcd  16431  oddprmgt2  16626  unbenlem  16836  infpnlem1  16838  prmgaplem6  16984  lmodvsdi  20836  lspsolvlem  21097  lbsextlem2  21114  gsummoncoe1  22252  cpmatmcllem  22662  mp2pm2mplem4  22753  1stccnp  23406  itg2le  25696  ewlkle  29679  clwlkclwwlklem2a  30073  3vfriswmgr  30353  frgrwopreg  30398  frgr2wwlk1  30404  frgrreg  30469  spansneleq  31645  elspansn4  31648  cvmdi  32399  atcvat3i  32471  mdsymlem3  32480  slmdvsdi  33297  satfv0  35552  satffunlem1lem1  35596  satffunlem2lem1  35598  mclsppslem  35777  dfon2lem8  35982  heicant  37852  areacirclem1  37905  areacirclem2  37906  areacirclem4  37908  areacirc  37910  fzmul  37938  cvlexch1  39584  hlrelat2  39659  cvrat3  39698  snatpsubN  40006  pmaple  40017  sn-sup2  42742  fzopredsuc  47565  gbegt5  48003