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  5585  tz7.7  6358  f1oweALT  7951  soseq  8138  onfununi  8310  odi  8543  omeu  8549  nndi  8587  inf3lem2  9582  axdc3lem2  10404  genpnmax  10960  mulclprlem  10972  distrlem5pr  10980  reclem4pr  11003  lemul12a  12040  sup2  12139  nnmulcl  12210  zbtwnre  12905  elfz0fzfz0  13594  fzofzim  13670  fzo1fzo0n0  13676  elincfzoext  13684  elfzodifsumelfzo  13692  le2sq2  14100  expnbnd  14197  swrdswrd  14670  swrdccat3blem  14704  climbdd  15638  dvdslegcd  16474  oddprmgt2  16669  unbenlem  16879  infpnlem1  16881  prmgaplem6  17027  lmodvsdi  20791  lspsolvlem  21052  lbsextlem2  21069  gsummoncoe1  22195  cpmatmcllem  22605  mp2pm2mplem4  22696  1stccnp  23349  itg2le  25640  ewlkle  29533  clwlkclwwlklem2a  29927  3vfriswmgr  30207  frgrwopreg  30252  frgr2wwlk1  30258  frgrreg  30323  spansneleq  31499  elspansn4  31502  cvmdi  32253  atcvat3i  32325  mdsymlem3  32334  slmdvsdi  33168  satfv0  35345  satffunlem1lem1  35389  satffunlem2lem1  35391  mclsppslem  35570  dfon2lem8  35778  heicant  37649  areacirclem1  37702  areacirclem2  37703  areacirclem4  37705  areacirc  37707  fzmul  37735  cvlexch1  39321  hlrelat2  39397  cvrat3  39436  snatpsubN  39744  pmaple  39755  sn-sup2  42479  fzopredsuc  47324  gbegt5  47762