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 452 . 2 ((𝜑𝜓) → (𝜒 → (𝜃𝜏)))
32ex 450 1 (𝜑 → (𝜓 → (𝜒 → (𝜃𝜏))))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 384 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 386 This theorem is referenced by:  exp4a  632  exp43  639  somo  5039  tz7.7  5718  f1oweALT  7112  onfununi  7398  odi  7619  omeu  7625  nndi  7663  inf3lem2  8486  axdc3lem2  9233  genpnmax  9789  mulclprlem  9801  distrlem5pr  9809  reclem4pr  9832  lemul12a  10841  sup2  10939  nnmulcl  11003  zbtwnre  11746  elfz0fzfz0  12401  fzofzim  12471  fzo1fzo0n0  12475  elincfzoext  12482  elfzodifsumelfzo  12490  le2sq2  12895  expnbnd  12949  swrdswrd  13414  swrdccat3blem  13448  climbdd  14352  dvdslegcd  15169  oddprmgt2  15354  unbenlem  15555  infpnlem1  15557  prmgaplem6  15703  lmodvsdi  18826  lspsolvlem  19082  lbsextlem2  19099  gsummoncoe1  19614  cpmatmcllem  20463  mp2pm2mplem4  20554  1stccnp  21205  itg2le  23446  ewlkle  26405  clwlkclwwlklem2a  26800  3vfriswmgr  27040  frgrreg  27140  spansneleq  28317  elspansn4  28320  cvmdi  29071  atcvat3i  29143  mdsymlem3  29152  slmdvsdi  29595  mclsppslem  31241  dfon2lem8  31449  soseq  31505  nodenselem5  31601  heicant  33115  areacirclem1  33171  areacirclem2  33172  areacirclem4  33174  areacirc  33176  fzmul  33208  cvlexch1  34134  hlrelat2  34208  cvrat3  34247  snatpsubN  34555  pmaple  34566  fzopredsuc  40660  gbegt5  40974
 Copyright terms: Public domain W3C validator