Theorem exp4b 436

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  exp4a  437  exp43  442  somo  5598  tz7.7  6381  f1oweALT  7973  soseq  8160  onfununi  8333  odi  8571  omeu  8577  nndi  8616  inf3lem2  9614  axdc3lem2  10510  genpnmax  11073  mulclprlem  11085  distrlem5pr  11093  reclem4pr  11116  lemul12a  12156  sup2  12254  nnmulcl  12340  zbtwnre  13054  elfz0fzfz0  13747  fzofzim  13824  fzo1fzo0n0  13830  elincfzoext  13838  elfzodifsumelfzo  13846  le2sq2  14258  expnbnd  14356  swrdswrd  14834  swrdccat3blem  14868  climbdd  15819  dvdslegcd  16654  oddprmgt2  16855  unbenlem  17066  infpnlem1  17068  prmgaplem6  17214  lmodvsdi  21140  lspsolvlem  21400  lbsextlem2  21417  gsummoncoe1  22606  cpmatmcllem  23016  mp2pm2mplem4  23107  1stccnp  23761  itg2le  26040  ewlkle  30168  clwlkclwwlklem2a  30571  3vfriswmgr  30861  frgrwopreg  30906  frgr2wwlk1  30912  frgrreg  30977  spansneleq  32154  elspansn4  32157  cvmdi  32908  atcvat3i  32980  mdsymlem3  32989  slmdvsdi  33758  satfv0  36092  satffunlem1lem1  36136  satffunlem2lem1  36138  mclsppslem  36317  dfon2lem8  36522  heicant  38541  areacirclem1  38594  areacirclem2  38595  areacirclem4  38597  areacirc  38599  fzmul  38643  cvlexch1  40353  hlrelat2  40428  cvrat3  40467  snatpsubN  40775  pmaple  40786  sn-sup2  43523  fzopredsuc  48338  muldvdsfacgt  48400  muldvdsfacm1  48401  gbegt5  48803