MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  impexp 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  1377  ax12bOLD  1697  2sb6  2146  2sb6rf  2152  2exsb  2166  eu2  2263  moanim  2294  2eu6  2323  r2alf  2684  r3al  2706  r19.23t  2763  ceqsralt  2922  ralrab  3039  ralrab2  3043  euind  3064  reu2  3065  reu3  3067  rmo4  3070  reuind  3080  2reu5lem3  3084  rmo2  3189  rmo3  3191  ralss  3352  rabss  3363  raldifb  3430  unissb  3987  elintrab  4004  ssintrab  4015  dftr5  4246  axrep5  4266  reusv2lem4  4667  reusv2  4669  reusv3  4671  ordunisuc2  4764  dfom2  4787  raliunxp  4954  fununi  5457  dff13  5943  dfsmo2  6545  qliftfun  6925  dfsup2  7382  wemapso2lem  7452  iscard2  7796  acnnum  7866  aceq1  7931  dfac9  7949  dfacacn  7954  axgroth6  8636  sstskm  8650  infm3  9899  prime  10282  raluz  10457  raluz2  10458  nnwos  10476  ralrp  10562  facwordi  11507  rexuzre  12083  limsupgle  12198  ello12  12237  elo12  12248  lo1resb  12285  rlimresb  12286  o1resb  12287  isprm2  13014  isprm4  13016  acsfn2  13815  pgpfac1  15565  isirred2  15733  isdomn2  16286  ist1-2  17333  isnrm2  17344  dfcon2  17403  1stccn  17447  iskgen3  17502  hausdiag  17598  cnflf  17955  txflf  17959  cnfcf  17995  metcnp  18461  caucfil  19107  ovolgelb  19243  ismbl  19289  dyadmbllem  19358  itg2leub  19493  ellimc3  19633  mdegleb  19854  jensen  20694  dchrelbas2  20888  dchrelbas3  20889  nmoubi  22121  nmobndseqi  22128  nmobndseqiOLD  22129  h1dei  22900  nmopub  23259  nmfnleub  23276  mdsl1i  23672  mdsl2i  23673  elat2  23691  rmo3f  23826  rmo4fOLD  23827  climuzcnv  24887  axextprim  24929  biimpexp  24952  dfpo2  25136  dfon2lem8  25170  predreseq  25203  dffun10  25477  filnetlem4  26101  raldifsni  26425  dford4  26791  fnwe2lem2  26817  islindf4  26977  isdomn3  27192  pm11.62  27262  2sbc6g  27284  2rexsb  27616  2rexrsb  27617  rmoanim  27625  impexp3a  27939  dfvd2  28012  dfvd3  28024  bnj115  28428  bnj1109  28495  bnj1533  28561  bnj580  28622  bnj864  28631  bnj865  28632  bnj1049  28681  bnj1090  28686  bnj1093  28687  bnj1133  28696  bnj1171  28707  2sb6NEW7  28943  2sb6rfOLD7  29079  2exsbOLD7  29084  isat3  29422  isltrn2N  30234  cdlemefrs29bpre0  30510  cdleme32fva  30551
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