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  5579  tz7.7  6351  f1oweALT  7926  soseq  8111  onfununi  8283  odi  8516  omeu  8522  nndi  8561  inf3lem2  9550  axdc3lem2  10373  genpnmax  10930  mulclprlem  10942  distrlem5pr  10950  reclem4pr  10973  lemul12a  12011  sup2  12110  nnmulcl  12181  zbtwnre  12871  elfz0fzfz0  13561  fzofzim  13637  fzo1fzo0n0  13643  elincfzoext  13651  elfzodifsumelfzo  13659  le2sq2  14070  expnbnd  14167  swrdswrd  14640  swrdccat3blem  14674  climbdd  15607  dvdslegcd  16443  oddprmgt2  16638  unbenlem  16848  infpnlem1  16850  prmgaplem6  16996  lmodvsdi  20848  lspsolvlem  21109  lbsextlem2  21126  gsummoncoe1  22264  cpmatmcllem  22674  mp2pm2mplem4  22765  1stccnp  23418  itg2le  25708  ewlkle  29691  clwlkclwwlklem2a  30085  3vfriswmgr  30365  frgrwopreg  30410  frgr2wwlk1  30416  frgrreg  30481  spansneleq  31657  elspansn4  31660  cvmdi  32411  atcvat3i  32483  mdsymlem3  32492  slmdvsdi  33308  satfv0  35571  satffunlem1lem1  35615  satffunlem2lem1  35617  mclsppslem  35796  dfon2lem8  36001  heicant  37900  areacirclem1  37953  areacirclem2  37954  areacirclem4  37956  areacirc  37958  fzmul  37986  cvlexch1  39698  hlrelat2  39773  cvrat3  39812  snatpsubN  40120  pmaple  40131  sn-sup2  42855  fzopredsuc  47677  gbegt5  48115