Theorem exp4b 435

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

Syntax hints:   → wi 4   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  exp4a  436  exp43  441  somo  5599  tz7.7  6376  f1oweALT  7957  soseq  8143  onfununi  8316  odi  8552  omeu  8558  nndi  8597  inf3lem2  9586  axdc3lem2  10423  genpnmax  10980  mulclprlem  10992  distrlem5pr  11000  reclem4pr  11023  lemul12a  12064  sup2  12162  nnmulcl  12248  zbtwnre  12961  elfz0fzfz0  13652  fzofzim  13729  fzo1fzo0n0  13735  elincfzoext  13743  elfzodifsumelfzo  13751  le2sq2  14162  expnbnd  14259  swrdswrd  14732  swrdccat3blem  14766  climbdd  15713  dvdslegcd  16552  oddprmgt2  16748  unbenlem  16958  infpnlem1  16960  prmgaplem6  17106  lmodvsdi  20975  lspsolvlem  21235  lbsextlem2  21252  gsummoncoe1  22429  cpmatmcllem  22836  mp2pm2mplem4  22927  1stccnp  23580  itg2le  25859  ewlkle  29864  clwlkclwwlklem2a  30258  3vfriswmgr  30538  frgrwopreg  30583  frgr2wwlk1  30589  frgrreg  30654  spansneleq  31831  elspansn4  31834  cvmdi  32585  atcvat3i  32657  mdsymlem3  32666  slmdvsdi  33448  satfv0  35721  satffunlem1lem1  35765  satffunlem2lem1  35767  mclsppslem  35946  dfon2lem8  36151  heicant  38166  areacirclem1  38219  areacirclem2  38220  areacirclem4  38222  areacirc  38224  fzmul  38252  cvlexch1  39964  hlrelat2  40039  cvrat3  40078  snatpsubN  40386  pmaple  40397  sn-sup2  43125  fzopredsuc  47916  muldvdsfacgt  47978  muldvdsfacm1  47979  gbegt5  48381