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

Theorem exp4b 607
Description: An exportation inference. (Contributed by NM, 26-Apr-1994.) (Proof shortened by Wolf Lammen, 23-Nov-2012.)
Hypothesis
Ref Expression
exp4b.1  |-  ( (
ph  /\  ps )  ->  ( ( ch  /\  th )  ->  ta )
)
Assertion
Ref Expression
exp4b  |-  ( ph  ->  ( ps  ->  ( ch  ->  ( th  ->  ta ) ) ) )

Proof of Theorem exp4b
StepHypRef Expression
1 exp4b.1 . . 3  |-  ( (
ph  /\  ps )  ->  ( ( ch  /\  th )  ->  ta )
)
21ex 434 . 2  |-  ( ph  ->  ( ps  ->  (
( ch  /\  th )  ->  ta ) ) )
32exp4a 606 1  |-  ( ph  ->  ( ps  ->  ( ch  ->  ( th  ->  ta ) ) ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369
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 185  df-an 371
This theorem is referenced by:  exp43  612  reuss2  3785  somo  4843  tz7.7  4913  f1oweALT  6783  onfununi  7030  odi  7246  omeu  7252  nndi  7290  inf3lem2  8063  axdc3lem2  8848  genpnmax  9402  mulclprlem  9414  distrlem5pr  9422  reclem4pr  9445  lemul12a  10421  sup2  10519  nnmulcl  10579  zbtwnre  11205  elfz0fzfz0  11804  fzo1fzo0n0  11862  fzofzim  11867  elincfzoext  11876  elfzodifsumelfzo  11884  le2sq2  12245  expnbnd  12297  swrdswrd  12696  swrdccat3blem  12731  climbdd  13505  dvdslegcd  14165  unbenlem  14437  infpnlem1  14439  lmodvsdi  17661  lspsolvlem  17914  lbsextlem2  17931  gsummoncoe1  18472  cpmatmcllem  19345  mp2pm2mplem4  19436  1stccnp  20088  itg2le  22271  wlkiswwlk1  24816  clwlkisclwwlklem2a  24911  el2spthonot  24996  spansneleq  26614  elspansn4  26617  cvmdi  27369  atcvat3i  27441  mdsymlem3  27450  slmdvsdi  27910  mclsppslem  29118  dfon2lem8  29396  soseq  29508  nodenselem5  29619  heicant  30211  dvtanlem  30226  areacirclem1  30269  areacirclem2  30270  areacirclem4  30272  areacirc  30274  fzmul  30395  el2fzo  32561  cvlexch1  35154  hlrelat2  35228  cvrat3  35267  snatpsubN  35575  pmaple  35586
  Copyright terms: Public domain W3C validator