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  5613  tz7.7  6393  f1oweALT  7978  soseq  8164  onfununi  8337  odi  8573  omeu  8579  nndi  8618  inf3lem2  9608  axdc3lem2  10453  genpnmax  11010  mulclprlem  11022  distrlem5pr  11030  reclem4pr  11053  lemul12a  12091  sup2  12189  nnmulcl  12275  zbtwnre  12988  elfz0fzfz0  13680  fzofzim  13757  fzo1fzo0n0  13763  elincfzoext  13771  elfzodifsumelfzo  13779  le2sq2  14191  expnbnd  14288  swrdswrd  14766  swrdccat3blem  14800  climbdd  15749  dvdslegcd  16587  oddprmgt2  16783  unbenlem  16993  infpnlem1  16995  prmgaplem6  17141  lmodvsdi  21043  lspsolvlem  21303  lbsextlem2  21320  gsummoncoe1  22505  cpmatmcllem  22912  mp2pm2mplem4  23003  1stccnp  23656  itg2le  25935  ewlkle  29992  clwlkclwwlklem2a  30386  3vfriswmgr  30666  frgrwopreg  30711  frgr2wwlk1  30717  frgrreg  30782  spansneleq  31959  elspansn4  31962  cvmdi  32713  atcvat3i  32785  mdsymlem3  32794  slmdvsdi  33566  satfv0  35871  satffunlem1lem1  35915  satffunlem2lem1  35917  mclsppslem  36096  dfon2lem8  36301  heicant  38347  areacirclem1  38400  areacirclem2  38401  areacirclem4  38403  areacirc  38405  fzmul  38433  cvlexch1  40143  hlrelat2  40218  cvrat3  40257  snatpsubN  40565  pmaple  40576  sn-sup2  43306  fzopredsuc  48102  muldvdsfacgt  48164  muldvdsfacm1  48165  gbegt5  48567