MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  exp4b Structured version   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  3613  somo  4529  tz7.7  4599  f1oweALT  6066  onfununi  6595  odi  6814  omeu  6820  nndi  6858  inf3lem2  7576  axdc3lem2  8323  genpnmax  8876  mulclprlem  8888  distrlem5pr  8896  reclem4pr  8919  mulcmpblnr  8941  lemul12a  9860  sup2  9956  nnmulcl  10015  zbtwnre  10564  le2sq2  11449  expnbnd  11500  climbdd  12457  dvdslegcd  13008  unbenlem  13268  infpnlem1  13270  lmodvsdi  15965  lspsolvlem  16206  lbsextlem2  16223  1stccnp  17517  itg2le  19623  spansneleq  23064  elspansn4  23067  cvmdi  23819  atcvat3i  23891  mdsymlem3  23900  dfon2lem8  25409  soseq  25521  nodenselem5  25632  areacirclem2  26282  areacirclem3  26283  areacirclem4  26284  areacirclem5  26286  areacirc  26288  fzmul  26435  elfz0fzfz0  28098  fzo1fzo0n0  28111  swrd0swrd  28163  swrdswrd  28165  swrdccat3blem  28184  2cshw1lem1  28214  cshweqdif2s  28234  el2spthonot  28290  cvlexch1  30063  hlrelat2  30137  cvrat3  30176  snatpsubN  30484  pmaple  30495
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