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

Theorem exp4b 607
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 606 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  612  reuss2  3778  somo  4834  tz7.7  4904  f1oweALT  6765  onfununi  7009  odi  7225  omeu  7231  nndi  7269  inf3lem2  8042  axdc3lem2  8827  genpnmax  9381  mulclprlem  9393  distrlem5pr  9401  reclem4pr  9424  lemul12a  10396  sup2  10495  nnmulcl  10555  zbtwnre  11176  elfz0fzfz0  11773  fzo1fzo0n0  11828  fzofzim  11833  elfzodifsumelfzo  11846  le2sq2  12207  expnbnd  12259  swrdswrd  12644  swrdccat3blem  12679  climbdd  13453  dvdslegcd  14009  unbenlem  14281  infpnlem1  14283  lmodvsdi  17318  lspsolvlem  17571  lbsextlem2  17588  gsummoncoe1  18117  cpmatmcllem  18986  mp2pm2mplem4  19077  1stccnp  19729  itg2le  21881  wlkiswwlk1  24366  clwlkisclwwlklem2a  24461  el2spthonot  24546  spansneleq  26164  elspansn4  26167  cvmdi  26919  atcvat3i  26991  mdsymlem3  27000  slmdvsdi  27420  dfon2lem8  28799  soseq  28911  nodenselem5  29022  heicant  29626  dvtanlem  29641  areacirclem1  29684  areacirclem2  29685  areacirclem4  29687  areacirc  29689  fzmul  29836  el2fzo  31808  cvlexch1  34125  hlrelat2  34199  cvrat3  34238  snatpsubN  34546  pmaple  34557
  Copyright terms: Public domain W3C validator