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

Theorem impexp 433
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 431 . 2  |-  ( ( ( ph  /\  ps )  ->  ch )  -> 
( ph  ->  ( ps 
->  ch ) ) )
2 pm3.31 432 . 2  |-  ( (
ph  ->  ( ps  ->  ch ) )  ->  (
( ph  /\  ps )  ->  ch ) )
31, 2impbii 180 1  |-  ( ( ( ph  /\  ps )  ->  ch )  <->  ( ph  ->  ( ps  ->  ch ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    /\ wa 358
This theorem is referenced by:  pm4.14  561  nan  563  pm4.87  567  imp4a  572  exp4a  589  imdistan  670  pm5.3  692  pm5.6  878  exp3acom23g  1361  ax12bOLD  1675  2sb6  2065  2sb6rf  2070  2exsb  2084  eu2  2181  moanim  2212  2eu6  2241  r2alf  2591  r3al  2613  r19.23t  2670  ceqsralt  2824  ralrab  2940  ralrab2  2944  euind  2965  reu2  2966  reu3  2968  rmo4  2971  reuind  2981  2reu5lem3  2985  rmo2  3089  rmo3  3091  ralss  3252  rabss  3263  unissb  3873  elintrab  3890  ssintrab  3901  dftr5  4132  axrep5  4152  reusv2lem4  4554  reusv2  4556  reusv3  4558  ordunisuc2  4651  dfom2  4674  raliunxp  4841  fununi  5332  dff13  5799  dfsmo2  6380  qliftfun  6759  dfsup2  7211  wemapso2lem  7281  iscard2  7625  acnnum  7695  aceq1  7760  dfac9  7778  dfacacn  7783  axgroth6  8466  sstskm  8480  infm3  9729  prime  10108  raluz  10283  raluz2  10284  nnwos  10302  ralrp  10388  facwordi  11318  rexuzre  11852  limsupgle  11967  ello12  12006  elo12  12017  lo1resb  12054  rlimresb  12055  o1resb  12056  isprm2  12782  isprm4  12784  acsfn2  13581  pgpfac1  15331  isirred2  15499  isdomn2  16056  ist1-2  17091  isnrm2  17102  dfcon2  17161  1stccn  17205  iskgen3  17260  hausdiag  17355  cnflf  17713  txflf  17717  cnfcf  17753  metcnp  18103  caucfil  18725  ovolgelb  18855  ismbl  18901  dyadmbllem  18970  itg2leub  19105  ellimc3  19245  mdegleb  19466  jensen  20299  dchrelbas2  20492  dchrelbas3  20493  nmoubi  21366  nmobndseqi  21373  nmobndseqiOLD  21374  h1dei  22145  nmopub  22504  nmfnleub  22521  mdsl1i  22917  mdsl2i  22918  elat2  22936  rmo3f  23194  rmo4fOLD  23195  climuzcnv  24019  axextprim  24062  biimpexp  24085  dfpo2  24183  dfon2lem8  24217  predreseq  24250  dffun10  24524  filnetlem4  26433  raldifsni  26856  dford4  27225  fnwe2lem2  27251  islindf4  27411  isdomn3  27626  pm11.62  27696  2sbc6g  27718  2rexsb  28051  2rexrsb  28052  rmoanim  28060  impexp3a  28574  dfvd2  28647  dfvd3  28659  bnj115  29067  bnj1109  29134  bnj1533  29200  bnj580  29261  bnj864  29270  bnj865  29271  bnj1049  29320  bnj1090  29325  bnj1093  29326  bnj1133  29335  bnj1171  29346  2sb6NEW7  29582  2sb6rfOLD7  29718  2exsbOLD7  29723  ax12conj2  29730  a12study8  29741  isat3  30119  isltrn2N  30931  cdlemefrs29bpre0  31207  cdleme32fva  31248
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 177  df-an 360
  Copyright terms: Public domain W3C validator