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  5588  tz7.7  6361  f1oweALT  7954  soseq  8141  onfununi  8313  odi  8546  omeu  8552  nndi  8590  inf3lem2  9589  axdc3lem2  10411  genpnmax  10967  mulclprlem  10979  distrlem5pr  10987  reclem4pr  11010  lemul12a  12047  sup2  12146  nnmulcl  12217  zbtwnre  12912  elfz0fzfz0  13601  fzofzim  13677  fzo1fzo0n0  13683  elincfzoext  13691  elfzodifsumelfzo  13699  le2sq2  14107  expnbnd  14204  swrdswrd  14677  swrdccat3blem  14711  climbdd  15645  dvdslegcd  16481  oddprmgt2  16676  unbenlem  16886  infpnlem1  16888  prmgaplem6  17034  lmodvsdi  20798  lspsolvlem  21059  lbsextlem2  21076  gsummoncoe1  22202  cpmatmcllem  22612  mp2pm2mplem4  22703  1stccnp  23356  itg2le  25647  ewlkle  29540  clwlkclwwlklem2a  29934  3vfriswmgr  30214  frgrwopreg  30259  frgr2wwlk1  30265  frgrreg  30330  spansneleq  31506  elspansn4  31509  cvmdi  32260  atcvat3i  32332  mdsymlem3  32341  slmdvsdi  33175  satfv0  35352  satffunlem1lem1  35396  satffunlem2lem1  35398  mclsppslem  35577  dfon2lem8  35785  heicant  37656  areacirclem1  37709  areacirclem2  37710  areacirclem4  37712  areacirc  37714  fzmul  37742  cvlexch1  39328  hlrelat2  39404  cvrat3  39443  snatpsubN  39751  pmaple  39762  sn-sup2  42486  fzopredsuc  47328  gbegt5  47766