Theorem exp4b 431

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

Syntax hints:   → wi 4   ∧ wa 396

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 397

This theorem is referenced by:  exp4a  432  exp43  437  somo  5541  tz7.7  6296  f1oweALT  7824  onfununi  8181  odi  8419  omeu  8425  nndi  8463  inf3lem2  9396  axdc3lem2  10216  genpnmax  10772  mulclprlem  10784  distrlem5pr  10792  reclem4pr  10815  lemul12a  11842  sup2  11940  nnmulcl  12006  zbtwnre  12695  elfz0fzfz0  13370  fzofzim  13443  fzo1fzo0n0  13447  elincfzoext  13454  elfzodifsumelfzo  13462  le2sq2  13863  expnbnd  13956  swrdswrd  14427  swrdccat3blem  14461  climbdd  15392  dvdslegcd  16220  oddprmgt2  16413  unbenlem  16618  infpnlem1  16620  prmgaplem6  16766  lmodvsdi  20155  lspsolvlem  20413  lbsextlem2  20430  gsummoncoe1  21484  cpmatmcllem  21876  mp2pm2mplem4  21967  1stccnp  22622  itg2le  24913  ewlkle  27981  clwlkclwwlklem2a  28371  3vfriswmgr  28651  frgrwopreg  28696  frgr2wwlk1  28702  frgrreg  28767  spansneleq  29941  elspansn4  29944  cvmdi  30695  atcvat3i  30767  mdsymlem3  30776  slmdvsdi  31477  satfv0  33329  satffunlem1lem1  33373  satffunlem2lem1  33375  mclsppslem  33554  dfon2lem8  33775  soseq  33812  heicant  35821  areacirclem1  35874  areacirclem2  35875  areacirclem4  35877  areacirc  35879  fzmul  35908  cvlexch1  37349  hlrelat2  37424  cvrat3  37463  snatpsubN  37771  pmaple  37782  sn-sup2  40446  fzopredsuc  44826  gbegt5  45224