Theorem exp4b 434

Description: An exportation inference. (Contributed by NM, 26-Apr-1994.) (Proof shortened by Wolf Lammen, 23-Nov-2012.) Shorten exp4a 435. (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 419	. 2 ⊢ ((𝜑 ∧ 𝜓) → (𝜒 → (𝜃 → 𝜏)))
3	2	ex 416	1 ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏))))

Syntax hints:   → wi 4   ∧ wa 399

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 209  df-an 400

This theorem is referenced by:  exp4a  435  exp43  440  somo  5592  tz7.7  6368  f1oweALT  7949  soseq  8134  onfununi  8307  odi  8543  omeu  8549  nndi  8588  inf3lem2  9581  axdc3lem2  10405  genpnmax  10962  mulclprlem  10974  distrlem5pr  10982  reclem4pr  11005  lemul12a  12046  sup2  12145  nnmulcl  12231  zbtwnre  12944  elfz0fzfz0  13635  fzofzim  13712  fzo1fzo0n0  13718  elincfzoext  13726  elfzodifsumelfzo  13734  le2sq2  14145  expnbnd  14242  swrdswrd  14715  swrdccat3blem  14749  climbdd  15682  dvdslegcd  16521  oddprmgt2  16717  unbenlem  16927  infpnlem1  16929  prmgaplem6  17075  lmodvsdi  20932  lspsolvlem  21192  lbsextlem2  21209  gsummoncoe1  22351  cpmatmcllem  22758  mp2pm2mplem4  22849  1stccnp  23502  itg2le  25781  ewlkle  29752  clwlkclwwlklem2a  30146  3vfriswmgr  30426  frgrwopreg  30471  frgr2wwlk1  30477  frgrreg  30542  spansneleq  31719  elspansn4  31722  cvmdi  32473  atcvat3i  32545  mdsymlem3  32554  slmdvsdi  33356  satfv0  35672  satffunlem1lem1  35716  satffunlem2lem1  35718  mclsppslem  35897  dfon2lem8  36102  heicant  38118  areacirclem1  38171  areacirclem2  38172  areacirclem4  38174  areacirc  38176  fzmul  38204  cvlexch1  39916  hlrelat2  39991  cvrat3  40030  snatpsubN  40338  pmaple  40349  sn-sup2  43077  fzopredsuc  47882  muldvdsfacgt  47944  muldvdsfacm1  47945  gbegt5  48347