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

Theorem impexp 434
Description: Import-export theorem. Part of Theorem *4.87 of [WhiteheadRussell] p. 122. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 24-Mar-2013.)
Assertion
Ref Expression
impexp  |-  ( ( ( ph  /\  ps )  ->  ch )  <->  ( ph  ->  ( ps  ->  ch ) ) )

Proof of Theorem impexp
StepHypRef Expression
1 pm3.3 432 . 2  |-  ( ( ( ph  /\  ps )  ->  ch )  -> 
( ph  ->  ( ps 
->  ch ) ) )
2 pm3.31 433 . 2  |-  ( (
ph  ->  ( ps  ->  ch ) )  ->  (
( ph  /\  ps )  ->  ch ) )
31, 2impbii 181 1  |-  ( ( ( ph  /\  ps )  ->  ch )  <->  ( ph  ->  ( ps  ->  ch ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    /\ wa 359
This theorem is referenced by:  pm4.14  562  nan  564  pm4.87  568  imp4a  573  exp4a  590  imdistan  671  pm5.3  693  pm5.6  879  exp3acom23g  1380  ax12bOLD  1702  2sb6  2188  2sb6rf  2194  2exsb  2208  eu2  2305  moanim  2336  2eu6  2365  r2alf  2732  r3al  2755  r19.23t  2812  ceqsralt  2971  ralrab  3088  ralrab2  3092  euind  3113  reu2  3114  reu3  3116  rmo4  3119  reuind  3129  2reu5lem3  3133  rmo2  3238  rmo3  3240  ralss  3401  rabss  3412  raldifb  3479  unissb  4037  elintrab  4054  ssintrab  4065  dftr5  4297  axrep5  4317  reusv2lem4  4719  reusv2  4721  reusv3  4723  ordunisuc2  4816  dfom2  4839  raliunxp  5006  fununi  5509  dff13  5996  dfsmo2  6601  qliftfun  6981  dfsup2  7439  wemapso2lem  7511  iscard2  7855  acnnum  7925  aceq1  7990  dfac9  8008  dfacacn  8013  axgroth6  8695  sstskm  8709  infm3  9959  prime  10342  raluz  10517  raluz2  10518  nnwos  10536  ralrp  10622  facwordi  11572  rexuzre  12148  limsupgle  12263  ello12  12302  elo12  12313  lo1resb  12350  rlimresb  12351  o1resb  12352  isprm2  13079  isprm4  13081  acsfn2  13880  pgpfac1  15630  isirred2  15798  isdomn2  16351  ist1-2  17403  isnrm2  17414  dfcon2  17474  1stccn  17518  iskgen3  17573  hausdiag  17669  cnflf  18026  txflf  18030  cnfcf  18066  metcnp  18563  caucfil  19228  ovolgelb  19368  ismbl  19414  dyadmbllem  19483  itg2leub  19618  ellimc3  19758  mdegleb  19979  jensen  20819  dchrelbas2  21013  dchrelbas3  21014  nmoubi  22265  nmobndseqi  22272  nmobndseqiOLD  22273  h1dei  23044  nmopub  23403  nmfnleub  23420  mdsl1i  23816  mdsl2i  23817  elat2  23835  rmo3f  23974  rmo4fOLD  23975  climuzcnv  25100  axextprim  25142  biimpexp  25165  dfpo2  25370  dfon2lem8  25409  predreseq  25446  dffun10  25751  filnetlem4  26401  raldifsni  26725  dford4  27091  fnwe2lem2  27117  islindf4  27276  isdomn3  27491  pm11.62  27561  2sbc6g  27583  2rexsb  27915  2rexrsb  27916  rmoanim  27924  impexp3a  28533  dfvd2  28608  dfvd3  28620  bnj115  29027  bnj1109  29094  bnj1533  29160  bnj580  29221  bnj864  29230  bnj865  29231  bnj1049  29280  bnj1090  29285  bnj1093  29286  bnj1133  29295  bnj1171  29306  2sb6NEW7  29547  2sb6rfOLD7  29699  2exsbOLD7  29704  isat3  30042  isltrn2N  30854  cdlemefrs29bpre0  31130  cdleme32fva  31171
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