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  6291  f1oweALT  7808  onfununi  8163  odi  8395  omeu  8401  nndi  8439  inf3lem2  9365  axdc3lem2  10208  genpnmax  10764  mulclprlem  10776  distrlem5pr  10784  reclem4pr  10807  lemul12a  11833  sup2  11931  nnmulcl  11997  zbtwnre  12685  elfz0fzfz0  13360  fzofzim  13432  fzo1fzo0n0  13436  elincfzoext  13443  elfzodifsumelfzo  13451  le2sq2  13852  expnbnd  13945  swrdswrd  14416  swrdccat3blem  14450  climbdd  15381  dvdslegcd  16209  oddprmgt2  16402  unbenlem  16607  infpnlem1  16609  prmgaplem6  16755  lmodvsdi  20144  lspsolvlem  20402  lbsextlem2  20419  gsummoncoe1  21473  cpmatmcllem  21865  mp2pm2mplem4  21956  1stccnp  22611  itg2le  24902  ewlkle  27970  clwlkclwwlklem2a  28358  3vfriswmgr  28638  frgrwopreg  28683  frgr2wwlk1  28689  frgrreg  28754  spansneleq  29928  elspansn4  29931  cvmdi  30682  atcvat3i  30754  mdsymlem3  30763  slmdvsdi  31464  satfv0  33316  satffunlem1lem1  33360  satffunlem2lem1  33362  mclsppslem  33541  dfon2lem8  33762  soseq  33799  heicant  35808  areacirclem1  35861  areacirclem2  35862  areacirclem4  35864  areacirc  35866  fzmul  35895  cvlexch1  37338  hlrelat2  37413  cvrat3  37452  snatpsubN  37760  pmaple  37771  sn-sup2  40436  fzopredsuc  44784  gbegt5  45182