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  5563  tz7.7  6332  f1oweALT  7904  soseq  8089  onfununi  8261  odi  8494  omeu  8500  nndi  8538  inf3lem2  9519  axdc3lem2  10339  genpnmax  10895  mulclprlem  10907  distrlem5pr  10915  reclem4pr  10938  lemul12a  11976  sup2  12075  nnmulcl  12146  zbtwnre  12841  elfz0fzfz0  13530  fzofzim  13606  fzo1fzo0n0  13612  elincfzoext  13620  elfzodifsumelfzo  13628  le2sq2  14039  expnbnd  14136  swrdswrd  14609  swrdccat3blem  14643  climbdd  15576  dvdslegcd  16412  oddprmgt2  16607  unbenlem  16817  infpnlem1  16819  prmgaplem6  16965  lmodvsdi  20816  lspsolvlem  21077  lbsextlem2  21094  gsummoncoe1  22221  cpmatmcllem  22631  mp2pm2mplem4  22722  1stccnp  23375  itg2le  25665  ewlkle  29582  clwlkclwwlklem2a  29973  3vfriswmgr  30253  frgrwopreg  30298  frgr2wwlk1  30304  frgrreg  30369  spansneleq  31545  elspansn4  31548  cvmdi  32299  atcvat3i  32371  mdsymlem3  32380  slmdvsdi  33179  satfv0  35390  satffunlem1lem1  35434  satffunlem2lem1  35436  mclsppslem  35615  dfon2lem8  35823  heicant  37694  areacirclem1  37747  areacirclem2  37748  areacirclem4  37750  areacirc  37752  fzmul  37780  cvlexch1  39366  hlrelat2  39441  cvrat3  39480  snatpsubN  39788  pmaple  39799  sn-sup2  42523  fzopredsuc  47353  gbegt5  47791