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

Theorem exp4b 418
Description: An exportation inference. (Contributed by NM, 26-Apr-1994.) (Proof shortened by Wolf Lammen, 23-Nov-2012.) Shorten exp4a 419. (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 401 . 2 ((𝜑𝜓) → (𝜒 → (𝜃𝜏)))
32ex 398 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 198  df-an 384
This theorem is referenced by:  exp4a  419  exp43  424  somo  5218  tz7.7  5903  f1oweALT  7320  onfununi  7612  odi  7834  omeu  7840  nndi  7878  inf3lem2  8711  axdc3lem2  9496  genpnmax  10052  mulclprlem  10064  distrlem5pr  10072  reclem4pr  10095  lemul12a  11104  sup2  11202  nnmulcl  11266  zbtwnre  12011  elfz0fzfz0  12674  fzofzim  12745  fzo1fzo0n0  12749  elincfzoext  12756  elfzodifsumelfzo  12764  le2sq2  13168  expnbnd  13222  swrdswrd  13691  swrdccat3blem  13726  climbdd  14632  dvdslegcd  15455  oddprmgt2  15639  unbenlem  15839  infpnlem1  15841  prmgaplem6  15987  lmodvsdi  19116  lspsolvlem  19376  lbsextlem2  19394  gsummoncoe1  19909  cpmatmcllem  20763  mp2pm2mplem4  20854  1stccnp  21506  itg2le  23747  ewlkle  26757  clwlkclwwlklem2a  27169  3vfriswmgr  27481  frgrwopreg  27526  frgr2wwlk1  27532  frgrreg  27610  spansneleq  28786  elspansn4  28789  cvmdi  29540  atcvat3i  29612  mdsymlem3  29621  slmdvsdi  30125  mclsppslem  31835  dfon2lem8  32048  soseq  32108  heicant  33794  areacirclem1  33849  areacirclem2  33850  areacirclem4  33852  areacirc  33854  fzmul  33885  cvlexch1  35152  hlrelat2  35227  cvrat3  35266  snatpsubN  35574  pmaple  35585  fzopredsuc  41885  gbegt5  42201
  Copyright terms: Public domain W3C validator