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 208  df-an 397

This theorem is referenced by:  exp4a  432  exp43  437  somo  5572  tz7.7  6343  f1oweALT  7921  soseq  8106  onfununi  8278  odi  8511  omeu  8517  nndi  8556  inf3lem2  9548  axdc3lem2  10371  genpnmax  10928  mulclprlem  10940  distrlem5pr  10948  reclem4pr  10971  lemul12a  12011  sup2  12110  nnmulcl  12196  zbtwnre  12894  elfz0fzfz0  13585  fzofzim  13662  fzo1fzo0n0  13668  elincfzoext  13676  elfzodifsumelfzo  13684  le2sq2  14095  expnbnd  14192  swrdswrd  14665  swrdccat3blem  14699  climbdd  15632  dvdslegcd  16471  oddprmgt2  16667  unbenlem  16877  infpnlem1  16879  prmgaplem6  17025  lmodvsdi  20882  lspsolvlem  21142  lbsextlem2  21159  gsummoncoe1  22301  cpmatmcllem  22708  mp2pm2mplem4  22799  1stccnp  23452  itg2le  25731  ewlkle  29699  clwlkclwwlklem2a  30093  3vfriswmgr  30373  frgrwopreg  30418  frgr2wwlk1  30424  frgrreg  30489  spansneleq  31666  elspansn4  31669  cvmdi  32420  atcvat3i  32492  mdsymlem3  32501  slmdvsdi  33303  satfv0  35593  satffunlem1lem1  35637  satffunlem2lem1  35639  mclsppslem  35818  dfon2lem8  36023  heicant  38029  areacirclem1  38082  areacirclem2  38083  areacirclem4  38085  areacirc  38087  fzmul  38115  cvlexch1  39827  hlrelat2  39902  cvrat3  39941  snatpsubN  40249  pmaple  40260  sn-sup2  42988  fzopredsuc  47794  muldvdsfacgt  47856  muldvdsfacm1  47857  gbegt5  48259