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  5578  tz7.7  6349  f1oweALT  7925  soseq  8109  onfununi  8281  odi  8514  omeu  8520  nndi  8559  inf3lem2  9550  axdc3lem2  10373  genpnmax  10930  mulclprlem  10942  distrlem5pr  10950  reclem4pr  10973  lemul12a  12013  sup2  12112  nnmulcl  12198  zbtwnre  12896  elfz0fzfz0  13587  fzofzim  13664  fzo1fzo0n0  13670  elincfzoext  13678  elfzodifsumelfzo  13686  le2sq2  14097  expnbnd  14194  swrdswrd  14667  swrdccat3blem  14701  climbdd  15634  dvdslegcd  16473  oddprmgt2  16669  unbenlem  16879  infpnlem1  16881  prmgaplem6  17027  lmodvsdi  20880  lspsolvlem  21140  lbsextlem2  21157  gsummoncoe1  22273  cpmatmcllem  22683  mp2pm2mplem4  22774  1stccnp  23427  itg2le  25706  ewlkle  29674  clwlkclwwlklem2a  30068  3vfriswmgr  30348  frgrwopreg  30393  frgr2wwlk1  30399  frgrreg  30464  spansneleq  31641  elspansn4  31644  cvmdi  32395  atcvat3i  32467  mdsymlem3  32476  slmdvsdi  33276  satfv0  35540  satffunlem1lem1  35584  satffunlem2lem1  35586  mclsppslem  35765  dfon2lem8  35970  heicant  37976  areacirclem1  38029  areacirclem2  38030  areacirclem4  38032  areacirc  38034  fzmul  38062  cvlexch1  39774  hlrelat2  39849  cvrat3  39888  snatpsubN  40196  pmaple  40207  sn-sup2  42936  fzopredsuc  47772  muldvdsfacgt  47834  muldvdsfacm1  47835  gbegt5  48237