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  5566  tz7.7  6337  f1oweALT  7910  soseq  8095  onfununi  8267  odi  8500  omeu  8506  nndi  8544  inf3lem2  9526  axdc3lem2  10349  genpnmax  10905  mulclprlem  10917  distrlem5pr  10925  reclem4pr  10948  lemul12a  11986  sup2  12085  nnmulcl  12156  zbtwnre  12846  elfz0fzfz0  13535  fzofzim  13611  fzo1fzo0n0  13617  elincfzoext  13625  elfzodifsumelfzo  13633  le2sq2  14044  expnbnd  14141  swrdswrd  14614  swrdccat3blem  14648  climbdd  15581  dvdslegcd  16417  oddprmgt2  16612  unbenlem  16822  infpnlem1  16824  prmgaplem6  16970  lmodvsdi  20820  lspsolvlem  21081  lbsextlem2  21098  gsummoncoe1  22224  cpmatmcllem  22634  mp2pm2mplem4  22725  1stccnp  23378  itg2le  25668  ewlkle  29586  clwlkclwwlklem2a  29980  3vfriswmgr  30260  frgrwopreg  30305  frgr2wwlk1  30311  frgrreg  30376  spansneleq  31552  elspansn4  31555  cvmdi  32306  atcvat3i  32378  mdsymlem3  32387  slmdvsdi  33191  satfv0  35423  satffunlem1lem1  35467  satffunlem2lem1  35469  mclsppslem  35648  dfon2lem8  35853  heicant  37715  areacirclem1  37768  areacirclem2  37769  areacirclem4  37771  areacirc  37773  fzmul  37801  cvlexch1  39447  hlrelat2  39522  cvrat3  39561  snatpsubN  39869  pmaple  39880  sn-sup2  42609  fzopredsuc  47447  gbegt5  47885