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

Theorem exp4b 590
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 423 . 2  |-  ( ph  ->  ( ps  ->  (
( ch  /\  th )  ->  ta ) ) )
32exp4a 589 1  |-  ( ph  ->  ( ps  ->  ( ch  ->  ( th  ->  ta ) ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358
This theorem is referenced by:  exp43  595  reuss2  3448  somo  4348  tz7.7  4418  f1oweALT  5851  onfununi  6358  odi  6577  omeu  6583  nndi  6621  inf3lem2  7330  axdc3lem2  8077  genpnmax  8631  mulclprlem  8643  distrlem5pr  8651  reclem4pr  8674  mulcmpblnr  8696  lemul12a  9614  sup2  9710  nnmulcl  9769  zbtwnre  10314  le2sq2  11179  expnbnd  11230  dvdslegcd  12695  unbenlem  12955  infpnlem1  12957  lmodvsdi  15650  lspsolvlem  15895  lbsextlem2  15912  1stccnp  17188  itg2le  19094  spansneleq  22149  elspansn4  22152  cvmdi  22904  atcvat3i  22976  mdsymlem3  22985  dfon2lem8  24146  soseq  24254  nodenselem5  24339  areacirclem2  24925  areacirclem3  24926  areacirclem4  24927  areacirclem5  24929  areacirc  24931  rspc2edv  24963  icmpmon  25816  fzmul  26443  cvlexch1  29518  hlrelat2  29592  cvrat3  29631  snatpsubN  29939  pmaple  29950
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177  df-an 360
  Copyright terms: Public domain W3C validator