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

Theorem exp4b 604
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 434 . 2  |-  ( ph  ->  ( ps  ->  (
( ch  /\  th )  ->  ta ) ) )
32exp4a 603 1  |-  ( ph  ->  ( ps  ->  ( ch  ->  ( th  ->  ta ) ) ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369
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 185  df-an 371
This theorem is referenced by:  exp43  609  reuss2  3627  somo  4671  tz7.7  4741  f1oweALT  6560  onfununi  6798  odi  7014  omeu  7020  nndi  7058  inf3lem2  7831  axdc3lem2  8616  genpnmax  9172  mulclprlem  9184  distrlem5pr  9192  reclem4pr  9215  mulcmpblnr  9237  lemul12a  10183  sup2  10282  nnmulcl  10341  zbtwnre  10947  elfz0fzfz0  11481  fzo1fzo0n0  11584  fzofzim  11589  elfzodifsumelfzo  11600  le2sq2  11937  expnbnd  11989  swrdswrd  12350  swrdccat3blem  12382  climbdd  13145  dvdslegcd  13696  unbenlem  13965  infpnlem1  13967  lmodvsdi  16951  lspsolvlem  17201  lbsextlem2  17218  1stccnp  19025  itg2le  21176  spansneleq  24908  elspansn4  24911  cvmdi  25663  atcvat3i  25735  mdsymlem3  25744  slmdvsdi  26164  dfon2lem8  27532  soseq  27644  nodenselem5  27755  heicant  28351  dvtanlem  28366  areacirclem1  28409  areacirclem2  28410  areacirclem4  28412  areacirc  28414  fzmul  28561  el2fzo  30137  wlkiswwlk1  30249  el2spthonot  30314  clwlkisclwwlklem2a  30372  cvlexch1  32695  hlrelat2  32769  cvrat3  32808  snatpsubN  33116  pmaple  33127
  Copyright terms: Public domain W3C validator