Theorem exp4b 433

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

Syntax hints:   → wi 4   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  exp4a  434  exp43  439  somo  5510  tz7.7  6217  f1oweALT  7673  onfununi  7978  odi  8205  omeu  8211  nndi  8249  inf3lem2  9092  axdc3lem2  9873  genpnmax  10429  mulclprlem  10441  distrlem5pr  10449  reclem4pr  10472  lemul12a  11498  sup2  11597  nnmulcl  11662  zbtwnre  12347  elfz0fzfz0  13013  fzofzim  13085  fzo1fzo0n0  13089  elincfzoext  13096  elfzodifsumelfzo  13104  le2sq2  13501  expnbnd  13594  swrdswrd  14067  swrdccat3blem  14101  climbdd  15028  dvdslegcd  15853  oddprmgt2  16043  unbenlem  16244  infpnlem1  16246  prmgaplem6  16392  lmodvsdi  19657  lspsolvlem  19914  lbsextlem2  19931  gsummoncoe1  20472  cpmatmcllem  21326  mp2pm2mplem4  21417  1stccnp  22070  itg2le  24340  ewlkle  27387  clwlkclwwlklem2a  27776  3vfriswmgr  28057  frgrwopreg  28102  frgr2wwlk1  28108  frgrreg  28173  spansneleq  29347  elspansn4  29350  cvmdi  30101  atcvat3i  30173  mdsymlem3  30182  slmdvsdi  30843  satfv0  32605  satffunlem1lem1  32649  satffunlem2lem1  32651  mclsppslem  32830  dfon2lem8  33035  soseq  33096  heicant  34942  areacirclem1  34997  areacirclem2  34998  areacirclem4  35000  areacirc  35002  fzmul  35031  cvlexch1  36479  hlrelat2  36554  cvrat3  36593  snatpsubN  36901  pmaple  36912  fzopredsuc  43543  gbegt5  43946