MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  exp4b Structured version   Visualization version   GIF version

Theorem exp4b 629
Description: An exportation inference. (Contributed by NM, 26-Apr-1994.) (Proof shortened by Wolf Lammen, 23-Nov-2012.) Shorten exp4a 630. (Revised by Wolf Lammen, 20-Jul-2021.)
Hypothesis
Ref Expression
exp4b.1 ((𝜑𝜓) → ((𝜒𝜃) → 𝜏))
Assertion
Ref Expression
exp4b (𝜑 → (𝜓 → (𝜒 → (𝜃𝜏))))

Proof of Theorem exp4b
StepHypRef Expression
1 exp4b.1 . . 3 ((𝜑𝜓) → ((𝜒𝜃) → 𝜏))
21expd 450 . 2 ((𝜑𝜓) → (𝜒 → (𝜃𝜏)))
32ex 448 1 (𝜑 → (𝜓 → (𝜒 → (𝜃𝜏))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382
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 195  df-an 384
This theorem is referenced by:  exp4a  630  exp43  637  somo  4979  tz7.7  5648  f1oweALT  7016  onfununi  7298  odi  7519  omeu  7525  nndi  7563  inf3lem2  8382  axdc3lem2  9129  genpnmax  9681  mulclprlem  9693  distrlem5pr  9701  reclem4pr  9724  lemul12a  10726  sup2  10824  nnmulcl  10886  zbtwnre  11614  elfz0fzfz0  12264  fzofzim  12333  fzo1fzo0n0  12337  elincfzoext  12344  elfzodifsumelfzo  12352  le2sq2  12752  expnbnd  12806  swrdswrd  13254  swrdccat3blem  13288  climbdd  14192  dvdslegcd  15006  oddprmgt2  15191  unbenlem  15392  infpnlem1  15394  prmgaplem6  15540  lmodvsdi  18651  lspsolvlem  18905  lbsextlem2  18922  gsummoncoe1  19437  cpmatmcllem  20280  mp2pm2mplem4  20371  1stccnp  21013  itg2le  23225  wlkiswwlk1  25980  clwlkisclwwlklem2a  26075  el2spthonot  26159  spansneleq  27615  elspansn4  27618  cvmdi  28369  atcvat3i  28441  mdsymlem3  28450  slmdvsdi  28901  mclsppslem  30536  dfon2lem8  30741  soseq  30797  nodenselem5  30886  heicant  32413  areacirclem1  32469  areacirclem2  32470  areacirclem4  32472  areacirc  32474  fzmul  32506  cvlexch1  33432  hlrelat2  33506  cvrat3  33545  snatpsubN  33853  pmaple  33864  fzopredsuc  39747  gbegt5  39984  ewlkle  40805  clwlkclwwlklem2a  41205  3vfriswmgr  41446  av-frgrareg  41546
  Copyright terms: Public domain W3C validator