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

Theorem exp4b 631
Description: An exportation inference. (Contributed by NM, 26-Apr-1994.) (Proof shortened by Wolf Lammen, 23-Nov-2012.) Shorten exp4a 632. (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 451 . 2 ((𝜑𝜓) → (𝜒 → (𝜃𝜏)))
32ex 449 1 (𝜑 → (𝜓 → (𝜒 → (𝜃𝜏))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383
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 197  df-an 385
This theorem is referenced by:  exp4a  632  exp43  639  somo  5098  tz7.7  5787  f1oweALT  7194  onfununi  7483  odi  7704  omeu  7710  nndi  7748  inf3lem2  8564  axdc3lem2  9311  genpnmax  9867  mulclprlem  9879  distrlem5pr  9887  reclem4pr  9910  lemul12a  10919  sup2  11017  nnmulcl  11081  zbtwnre  11824  elfz0fzfz0  12483  fzofzim  12554  fzo1fzo0n0  12558  elincfzoext  12565  elfzodifsumelfzo  12573  le2sq2  12979  expnbnd  13033  swrdswrd  13506  swrdccat3blem  13541  climbdd  14446  dvdslegcd  15273  oddprmgt2  15458  unbenlem  15659  infpnlem1  15661  prmgaplem6  15807  lmodvsdi  18934  lspsolvlem  19190  lbsextlem2  19207  gsummoncoe1  19722  cpmatmcllem  20571  mp2pm2mplem4  20662  1stccnp  21313  itg2le  23551  ewlkle  26557  clwlkclwwlklem2a  26964  3vfriswmgr  27258  frgrwopreg  27303  frgr2wwlk1  27309  frgrreg  27381  spansneleq  28557  elspansn4  28560  cvmdi  29311  atcvat3i  29383  mdsymlem3  29392  slmdvsdi  29896  mclsppslem  31606  dfon2lem8  31819  soseq  31879  heicant  33574  areacirclem1  33630  areacirclem2  33631  areacirclem4  33633  areacirc  33635  fzmul  33667  cvlexch1  34933  hlrelat2  35007  cvrat3  35046  snatpsubN  35354  pmaple  35365  fzopredsuc  41658  gbegt5  41974
  Copyright terms: Public domain W3C validator