Theorem exp4b 630

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

Syntax hints:   → wi 4   ∧ wa 383

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 196  df-an 385

This theorem is referenced by:  exp4a  631  exp43  638  somo  4993  tz7.7  5666  f1oweALT  7043  onfununi  7325  odi  7546  omeu  7552  nndi  7590  inf3lem2  8409  axdc3lem2  9156  genpnmax  9708  mulclprlem  9720  distrlem5pr  9728  reclem4pr  9751  lemul12a  10760  sup2  10858  nnmulcl  10920  zbtwnre  11662  elfz0fzfz0  12313  fzofzim  12382  fzo1fzo0n0  12386  elincfzoext  12393  elfzodifsumelfzo  12401  le2sq2  12801  expnbnd  12855  swrdswrd  13312  swrdccat3blem  13346  climbdd  14250  dvdslegcd  15064  oddprmgt2  15249  unbenlem  15450  infpnlem1  15452  prmgaplem6  15598  lmodvsdi  18709  lspsolvlem  18963  lbsextlem2  18980  gsummoncoe1  19495  cpmatmcllem  20342  mp2pm2mplem4  20433  1stccnp  21075  itg2le  23312  wlkiswwlk1  26218  clwlkisclwwlklem2a  26313  el2spthonot  26397  spansneleq  27813  elspansn4  27816  cvmdi  28567  atcvat3i  28639  mdsymlem3  28648  slmdvsdi  29099  mclsppslem  30734  dfon2lem8  30939  soseq  30995  nodenselem5  31084  heicant  32614  areacirclem1  32670  areacirclem2  32671  areacirclem4  32673  areacirc  32675  fzmul  32707  cvlexch1  33633  hlrelat2  33707  cvrat3  33746  snatpsubN  34054  pmaple  34065  fzopredsuc  39946  gbegt5  40183  ewlkle  40807  clwlkclwwlklem2a  41207  3vfriswmgr  41448  av-frgrareg  41548