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

Theorem impexp 435
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 433 . 2  |-  ( ( ( ph  /\  ps )  ->  ch )  -> 
( ph  ->  ( ps 
->  ch ) ) )
2 pm3.31 434 . 2  |-  ( (
ph  ->  ( ps  ->  ch ) )  ->  (
( ph  /\  ps )  ->  ch ) )
31, 2impbii 182 1  |-  ( ( ( ph  /\  ps )  ->  ch )  <->  ( ph  ->  ( ps  ->  ch ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 6    <-> wb 178    /\ wa 360
This theorem is referenced by:  pm4.14  564  nan  566  pm4.87  570  imp4a  575  exp4a  592  imdistan  673  pm5.3  695  pm5.6  883  exp3acom23g  1367  ax12b  1834  2sb6  2076  2sb6rf  2081  2exsb  2094  eu2  2141  moanim  2172  2eu6  2201  r2alf  2549  r3al  2571  r19.23t  2628  ceqsralt  2762  ralrab  2878  ralrab2  2882  euind  2903  reu2  2906  reu3  2908  rmo4  2911  reuind  2917  rmo3  3020  ralss  3181  rabss  3192  unissb  3798  elintrab  3815  ssintrab  3826  disjiun  3953  dftr5  4056  axrep5  4076  reusv2lem4  4475  reusv2  4477  reusv3  4479  ordunisuc2  4572  dfom2  4595  raliunxp  4778  fununi  5219  dff13  5682  dfsmo2  6297  qliftfun  6676  dfsup2  7128  wemapso2lem  7198  iscard2  7542  acnnum  7612  aceq1  7677  dfac9  7695  dfacacn  7700  axgroth6  8383  sstskm  8397  infm3  9646  prime  10024  raluz  10199  raluz2  10200  nnwos  10218  ralrp  10304  facwordi  11233  rexuzre  11766  limsupgle  11881  ello12  11920  elo12  11931  lo1resb  11968  rlimresb  11969  o1resb  11970  isprm2  12693  isprm4  12695  acsfn2  13492  pgpfac1  15242  isirred2  15410  isdomn2  15967  ist1-2  17002  isnrm2  17013  dfcon2  17072  1stccn  17116  iskgen3  17171  hausdiag  17266  cnflf  17624  txflf  17628  cnfcf  17664  metcnp  18014  caucfil  18636  ovolgelb  18766  ismbl  18812  dyadmbllem  18881  itg2leub  19016  ellimc3  19156  mdegleb  19377  jensen  20210  dchrelbas2  20403  dchrelbas3  20404  nmoubi  21275  nmobndseqi  21282  nmobndseqiOLD  21283  h1dei  22054  nmopub  22413  nmfnleub  22430  mdsl1i  22826  mdsl2i  22827  elat2  22845  climuzcnv  23341  axextprim  23384  biimpexp  23407  dfpo2  23448  dfon2lem8  23480  predreseq  23513  filnetlem4  25662  raldifsni  26085  dford4  26454  fnwe2lem2  26480  islindf4  26640  isdomn3  26855  pm11.62  26925  2sbc6g  26948  impexp3a  27291  dfvd2  27364  dfvd3  27376  bnj115  27763  bnj1109  27830  bnj1533  27896  bnj580  27957  bnj864  27966  bnj865  27967  bnj1049  28016  bnj1090  28021  bnj1093  28022  bnj1133  28031  bnj1171  28042  ax12conj2  28238  a12study8  28249  isat3  28627  isltrn2N  29439  cdlemefrs29bpre0  29715  cdleme32fva  29756
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10
This theorem depends on definitions:  df-bi 179  df-an 362
  Copyright terms: Public domain W3C validator