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  5634  tz7.7  6411  f1oweALT  7995  soseq  8182  onfununi  8379  odi  8615  omeu  8621  nndi  8659  inf3lem2  9666  axdc3lem2  10488  genpnmax  11044  mulclprlem  11056  distrlem5pr  11064  reclem4pr  11087  lemul12a  12122  sup2  12221  nnmulcl  12287  zbtwnre  12985  elfz0fzfz0  13669  fzofzim  13745  fzo1fzo0n0  13750  elincfzoext  13758  elfzodifsumelfzo  13766  le2sq2  14171  expnbnd  14267  swrdswrd  14739  swrdccat3blem  14773  climbdd  15704  dvdslegcd  16537  oddprmgt2  16732  unbenlem  16941  infpnlem1  16943  prmgaplem6  17089  lmodvsdi  20899  lspsolvlem  21161  lbsextlem2  21178  gsummoncoe1  22327  cpmatmcllem  22739  mp2pm2mplem4  22830  1stccnp  23485  itg2le  25788  ewlkle  29637  clwlkclwwlklem2a  30026  3vfriswmgr  30306  frgrwopreg  30351  frgr2wwlk1  30357  frgrreg  30422  spansneleq  31598  elspansn4  31601  cvmdi  32352  atcvat3i  32424  mdsymlem3  32433  slmdvsdi  33203  satfv0  35342  satffunlem1lem1  35386  satffunlem2lem1  35388  mclsppslem  35567  dfon2lem8  35771  heicant  37641  areacirclem1  37694  areacirclem2  37695  areacirclem4  37697  areacirc  37699  fzmul  37727  cvlexch1  39309  hlrelat2  39385  cvrat3  39424  snatpsubN  39732  pmaple  39743  sn-sup2  42477  fzopredsuc  47272  gbegt5  47685