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 206  df-an 396

This theorem is referenced by:  exp4a  431  exp43  436  somo  5531  tz7.7  6277  f1oweALT  7788  onfununi  8143  odi  8372  omeu  8378  nndi  8416  inf3lem2  9317  axdc3lem2  10138  genpnmax  10694  mulclprlem  10706  distrlem5pr  10714  reclem4pr  10737  lemul12a  11763  sup2  11861  nnmulcl  11927  zbtwnre  12615  elfz0fzfz0  13290  fzofzim  13362  fzo1fzo0n0  13366  elincfzoext  13373  elfzodifsumelfzo  13381  le2sq2  13782  expnbnd  13875  swrdswrd  14346  swrdccat3blem  14380  climbdd  15311  dvdslegcd  16139  oddprmgt2  16332  unbenlem  16537  infpnlem1  16539  prmgaplem6  16685  lmodvsdi  20061  lspsolvlem  20319  lbsextlem2  20336  gsummoncoe1  21385  cpmatmcllem  21775  mp2pm2mplem4  21866  1stccnp  22521  itg2le  24809  ewlkle  27875  clwlkclwwlklem2a  28263  3vfriswmgr  28543  frgrwopreg  28588  frgr2wwlk1  28594  frgrreg  28659  spansneleq  29833  elspansn4  29836  cvmdi  30587  atcvat3i  30659  mdsymlem3  30668  slmdvsdi  31370  satfv0  33220  satffunlem1lem1  33264  satffunlem2lem1  33266  mclsppslem  33445  dfon2lem8  33672  soseq  33730  heicant  35739  areacirclem1  35792  areacirclem2  35793  areacirclem4  35795  areacirc  35797  fzmul  35826  cvlexch1  37269  hlrelat2  37344  cvrat3  37383  snatpsubN  37691  pmaple  37702  sn-sup2  40360  fzopredsuc  44703  gbegt5  45101