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  7918  soseq  8102  onfununi  8274  odi  8507  omeu  8513  nndi  8552  inf3lem2  9541  axdc3lem2  10364  genpnmax  10921  mulclprlem  10933  distrlem5pr  10941  reclem4pr  10964  lemul12a  12004  sup2  12103  nnmulcl  12189  zbtwnre  12887  elfz0fzfz0  13578  fzofzim  13655  fzo1fzo0n0  13661  elincfzoext  13669  elfzodifsumelfzo  13677  le2sq2  14088  expnbnd  14185  swrdswrd  14658  swrdccat3blem  14692  climbdd  15625  dvdslegcd  16464  oddprmgt2  16660  unbenlem  16870  infpnlem1  16872  prmgaplem6  17018  lmodvsdi  20871  lspsolvlem  21132  lbsextlem2  21149  gsummoncoe1  22283  cpmatmcllem  22693  mp2pm2mplem4  22784  1stccnp  23437  itg2le  25716  ewlkle  29689  clwlkclwwlklem2a  30083  3vfriswmgr  30363  frgrwopreg  30408  frgr2wwlk1  30414  frgrreg  30479  spansneleq  31656  elspansn4  31659  cvmdi  32410  atcvat3i  32482  mdsymlem3  32491  slmdvsdi  33291  satfv0  35556  satffunlem1lem1  35600  satffunlem2lem1  35602  mclsppslem  35781  dfon2lem8  35986  heicant  37990  areacirclem1  38043  areacirclem2  38044  areacirclem4  38046  areacirc  38048  fzmul  38076  cvlexch1  39788  hlrelat2  39863  cvrat3  39902  snatpsubN  40210  pmaple  40221  sn-sup2  42950  fzopredsuc  47784  muldvdsfacgt  47846  muldvdsfacm1  47847  gbegt5  48249