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  3753  somo  4808  tz7.7  5468  f1oweALT  6792  onfununi  7072  odi  7292  omeu  7298  nndi  7336  inf3lem2  8144  axdc3lem2  8889  genpnmax  9440  mulclprlem  9452  distrlem5pr  9460  reclem4pr  9483  lemul12a  10471  sup2  10573  nnmulcl  10640  zbtwnre  11270  elfz0fzfz0  11903  fzo1fzo0n0  11965  fzofzim  11970  elincfzoext  11979  elfzodifsumelfzo  11987  le2sq2  12357  expnbnd  12408  swrdswrd  12819  swrdccat3blem  12854  climbdd  13735  dvdslegcd  14478  unbenlem  14852  infpnlem1  14854  prmgaplem6  15026  lmodvsdi  18114  lspsolvlem  18365  lbsextlem2  18382  gsummoncoe1  18898  cpmatmcllem  19741  mp2pm2mplem4  19832  1stccnp  20476  itg2le  22696  wlkiswwlk1  25417  clwlkisclwwlklem2a  25512  el2spthonot  25597  spansneleq  27222  elspansn4  27225  cvmdi  27976  atcvat3i  28048  mdsymlem3  28057  slmdvsdi  28539  mclsppslem  30230  dfon2lem8  30444  soseq  30500  nodenselem5  30580  heicant  31940  dvtanlemOLD  31956  areacirclem1  31997  areacirclem2  31998  areacirclem4  32000  areacirc  32002  fzmul  32034  cvlexch1  32864  hlrelat2  32938  cvrat3  32977  snatpsubN  33285  pmaple  33296  fzopredsuc  38591  gbegt5  38733
  Copyright terms: Public domain W3C validator