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  2189  2sb6rf  2195  2exsb  2209  eu2  2306  moanim  2337  2eu6  2366  r2alf  2740  r3al  2763  r19.23t  2820  ceqsralt  2979  ralrab  3096  ralrab2  3100  euind  3121  reu2  3122  reu3  3124  rmo4  3127  reuind  3137  2reu5lem3  3141  rmo2  3246  rmo3  3248  ralss  3409  rabss  3420  raldifb  3487  unissb  4045  elintrab  4062  ssintrab  4073  dftr5  4305  axrep5  4325  reusv2lem4  4727  reusv2  4729  reusv3  4731  ordunisuc2  4824  dfom2  4847  raliunxp  5014  fununi  5517  dff13  6004  dfsmo2  6609  qliftfun  6989  dfsup2  7447  wemapso2lem  7519  iscard2  7863  acnnum  7933  aceq1  7998  dfac9  8016  dfacacn  8021  axgroth6  8703  sstskm  8717  infm3  9967  prime  10350  raluz  10525  raluz2  10526  nnwos  10544  ralrp  10630  facwordi  11580  rexuzre  12156  limsupgle  12271  ello12  12310  elo12  12321  lo1resb  12358  rlimresb  12359  o1resb  12360  isprm2  13087  isprm4  13089  acsfn2  13888  pgpfac1  15638  isirred2  15806  isdomn2  16359  ist1-2  17411  isnrm2  17422  dfcon2  17482  1stccn  17526  iskgen3  17581  hausdiag  17677  cnflf  18034  txflf  18038  cnfcf  18074  metcnp  18571  caucfil  19236  ovolgelb  19376  ismbl  19422  dyadmbllem  19491  itg2leub  19626  ellimc3  19766  mdegleb  19987  jensen  20827  dchrelbas2  21021  dchrelbas3  21022  nmoubi  22273  nmobndseqi  22280  nmobndseqiOLD  22281  h1dei  23052  nmopub  23411  nmfnleub  23428  mdsl1i  23824  mdsl2i  23825  elat2  23843  rmo3f  23982  rmo4fOLD  23983  climuzcnv  25108  axextprim  25150  biimpexp  25173  dfpo2  25378  dfon2lem8  25417  predreseq  25454  dffun10  25759  filnetlem4  26410  raldifsni  26734  dford4  27100  fnwe2lem2  27126  islindf4  27285  isdomn3  27500  pm11.62  27570  2sbc6g  27592  2rexsb  27924  2rexrsb  27925  rmoanim  27933  impexp3a  28596  dfvd2  28671  dfvd3  28683  bnj115  29090  bnj1109  29157  bnj1533  29223  bnj580  29284  bnj864  29293  bnj865  29294  bnj1049  29343  bnj1090  29348  bnj1093  29349  bnj1133  29358  bnj1171  29369  2sb6NEW7  29610  2sb6rfOLD7  29762  2exsbOLD7  29767  isat3  30105  isltrn2N  30917  cdlemefrs29bpre0  31193  cdleme32fva  31234
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