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  5611  tz7.7  6389  f1oweALT  7979  soseq  8166  onfununi  8363  odi  8599  omeu  8605  nndi  8643  inf3lem2  9651  axdc3lem2  10473  genpnmax  11029  mulclprlem  11041  distrlem5pr  11049  reclem4pr  11072  lemul12a  12107  sup2  12206  nnmulcl  12272  zbtwnre  12970  elfz0fzfz0  13655  fzofzim  13731  fzo1fzo0n0  13736  elincfzoext  13744  elfzodifsumelfzo  13752  le2sq2  14158  expnbnd  14254  swrdswrd  14726  swrdccat3blem  14760  climbdd  15691  dvdslegcd  16524  oddprmgt2  16719  unbenlem  16929  infpnlem1  16931  prmgaplem6  17077  lmodvsdi  20852  lspsolvlem  21113  lbsextlem2  21130  gsummoncoe1  22261  cpmatmcllem  22673  mp2pm2mplem4  22764  1stccnp  23417  itg2le  25711  ewlkle  29552  clwlkclwwlklem2a  29946  3vfriswmgr  30226  frgrwopreg  30271  frgr2wwlk1  30277  frgrreg  30342  spansneleq  31518  elspansn4  31521  cvmdi  32272  atcvat3i  32344  mdsymlem3  32353  slmdvsdi  33165  satfv0  35338  satffunlem1lem1  35382  satffunlem2lem1  35384  mclsppslem  35563  dfon2lem8  35766  heicant  37637  areacirclem1  37690  areacirclem2  37691  areacirclem4  37693  areacirc  37695  fzmul  37723  cvlexch1  39304  hlrelat2  39380  cvrat3  39419  snatpsubN  39727  pmaple  39738  sn-sup2  42480  fzopredsuc  47308  gbegt5  47721