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

Theorem exp4b 610
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 435 . 2  |-  ( ph  ->  ( ps  ->  (
( ch  /\  th )  ->  ta ) ) )
32exp4a 609 1  |-  ( ph  ->  ( ps  ->  ( ch  ->  ( th  ->  ta ) ) ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 370
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 188  df-an 372
This theorem is referenced by:  exp43  615  reuss2  3759  somo  4809  tz7.7  5468  f1oweALT  6791  onfununi  7068  odi  7288  omeu  7294  nndi  7332  inf3lem2  8134  axdc3lem2  8879  genpnmax  9431  mulclprlem  9443  distrlem5pr  9451  reclem4pr  9474  lemul12a  10462  sup2  10565  nnmulcl  10632  zbtwnre  11262  elfz0fzfz0  11893  fzo1fzo0n0  11955  fzofzim  11960  elincfzoext  11969  elfzodifsumelfzo  11977  le2sq2  12347  expnbnd  12398  swrdswrd  12801  swrdccat3blem  12836  climbdd  13713  dvdslegcd  14452  unbenlem  14815  infpnlem1  14817  prmgaplem6  14989  lmodvsdi  18049  lspsolvlem  18300  lbsextlem2  18317  gsummoncoe1  18833  cpmatmcllem  19673  mp2pm2mplem4  19764  1stccnp  20408  itg2le  22574  wlkiswwlk1  25263  clwlkisclwwlklem2a  25358  el2spthonot  25443  spansneleq  27058  elspansn4  27061  cvmdi  27812  atcvat3i  27884  mdsymlem3  27893  slmdvsdi  28369  mclsppslem  30009  dfon2lem8  30223  soseq  30279  nodenselem5  30359  heicant  31679  dvtanlemOLD  31695  areacirclem1  31736  areacirclem2  31737  areacirclem4  31739  areacirc  31741  fzmul  31773  cvlexch1  32603  hlrelat2  32677  cvrat3  32716  snatpsubN  33024  pmaple  33035  fzopredsuc  38110  gbegt5  38252
  Copyright terms: Public domain W3C validator