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  5631  tz7.7  6410  f1oweALT  7997  soseq  8184  onfununi  8381  odi  8617  omeu  8623  nndi  8661  inf3lem2  9669  axdc3lem2  10491  genpnmax  11047  mulclprlem  11059  distrlem5pr  11067  reclem4pr  11090  lemul12a  12125  sup2  12224  nnmulcl  12290  zbtwnre  12988  elfz0fzfz0  13673  fzofzim  13749  fzo1fzo0n0  13754  elincfzoext  13762  elfzodifsumelfzo  13770  le2sq2  14175  expnbnd  14271  swrdswrd  14743  swrdccat3blem  14777  climbdd  15708  dvdslegcd  16541  oddprmgt2  16736  unbenlem  16946  infpnlem1  16948  prmgaplem6  17094  lmodvsdi  20883  lspsolvlem  21144  lbsextlem2  21161  gsummoncoe1  22312  cpmatmcllem  22724  mp2pm2mplem4  22815  1stccnp  23470  itg2le  25774  ewlkle  29623  clwlkclwwlklem2a  30017  3vfriswmgr  30297  frgrwopreg  30342  frgr2wwlk1  30348  frgrreg  30413  spansneleq  31589  elspansn4  31592  cvmdi  32343  atcvat3i  32415  mdsymlem3  32424  slmdvsdi  33221  satfv0  35363  satffunlem1lem1  35407  satffunlem2lem1  35409  mclsppslem  35588  dfon2lem8  35791  heicant  37662  areacirclem1  37715  areacirclem2  37716  areacirclem4  37718  areacirc  37720  fzmul  37748  cvlexch1  39329  hlrelat2  39405  cvrat3  39444  snatpsubN  39752  pmaple  39763  sn-sup2  42501  fzopredsuc  47335  gbegt5  47748