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  3635  somo  4680  tz7.7  4750  f1oweALT  6566  onfununi  6807  odi  7023  omeu  7029  nndi  7067  inf3lem2  7840  axdc3lem2  8625  genpnmax  9181  mulclprlem  9193  distrlem5pr  9201  reclem4pr  9224  mulcmpblnr  9246  lemul12a  10192  sup2  10291  nnmulcl  10350  zbtwnre  10956  elfz0fzfz0  11490  fzo1fzo0n0  11593  fzofzim  11598  elfzodifsumelfzo  11609  le2sq2  11946  expnbnd  11998  swrdswrd  12359  swrdccat3blem  12391  climbdd  13154  dvdslegcd  13705  unbenlem  13974  infpnlem1  13976  lmodvsdi  16976  lspsolvlem  17228  lbsextlem2  17245  1stccnp  19071  itg2le  21222  spansneleq  24978  elspansn4  24981  cvmdi  25733  atcvat3i  25805  mdsymlem3  25814  slmdvsdi  26236  dfon2lem8  27608  soseq  27720  nodenselem5  27831  heicant  28431  dvtanlem  28446  areacirclem1  28489  areacirclem2  28490  areacirclem4  28492  areacirc  28494  fzmul  28641  el2fzo  30217  wlkiswwlk1  30329  el2spthonot  30394  clwlkisclwwlklem2a  30452  gsummoncoe1  30848  mp2pm2mplem4  30924  cvlexch1  32978  hlrelat2  33052  cvrat3  33091  snatpsubN  33399  pmaple  33410
  Copyright terms: Public domain W3C validator