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

Theorem exp4b 591
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 424 . 2  |-  ( ph  ->  ( ps  ->  (
( ch  /\  th )  ->  ta ) ) )
32exp4a 590 1  |-  ( ph  ->  ( ps  ->  ( ch  ->  ( th  ->  ta ) ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359
This theorem is referenced by:  exp43  596  reuss2  3566  somo  4480  tz7.7  4550  f1oweALT  6015  onfununi  6541  odi  6760  omeu  6766  nndi  6804  inf3lem2  7519  axdc3lem2  8266  genpnmax  8819  mulclprlem  8831  distrlem5pr  8839  reclem4pr  8862  mulcmpblnr  8884  lemul12a  9802  sup2  9898  nnmulcl  9957  zbtwnre  10506  le2sq2  11386  expnbnd  11437  climbdd  12394  dvdslegcd  12945  unbenlem  13205  infpnlem1  13207  lmodvsdi  15902  lspsolvlem  16143  lbsextlem2  16160  1stccnp  17448  itg2le  19500  spansneleq  22922  elspansn4  22925  cvmdi  23677  atcvat3i  23749  mdsymlem3  23758  dfon2lem8  25172  soseq  25280  nodenselem5  25365  areacirclem2  25984  areacirclem3  25985  areacirclem4  25986  areacirclem5  25988  areacirc  25990  fzmul  26137  cvlexch1  29445  hlrelat2  29519  cvrat3  29558  snatpsubN  29866  pmaple  29877
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 178  df-an 361
  Copyright terms: Public domain W3C validator