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  1658  2sb6  2054  2sb6rf  2059  2exsb  2073  eu2  2170  moanim  2201  2eu6  2230  r2alf  2580  r3al  2602  r19.23t  2659  ceqsralt  2813  ralrab  2929  ralrab2  2933  euind  2954  reu2  2955  reu3  2957  rmo4  2960  reuind  2970  2reu5lem3  2974  rmo2  3078  rmo3  3080  ralss  3241  rabss  3252  unissb  3859  elintrab  3876  ssintrab  3887  dftr5  4118  axrep5  4138  reusv2lem4  4540  reusv2  4542  reusv3  4544  ordunisuc2  4637  dfom2  4660  raliunxp  4827  fununi  5318  dff13  5785  dfsmo2  6366  qliftfun  6745  dfsup2  7197  wemapso2lem  7267  iscard2  7611  acnnum  7681  aceq1  7746  dfac9  7764  dfacacn  7769  axgroth6  8452  sstskm  8466  infm3  9715  prime  10094  raluz  10269  raluz2  10270  nnwos  10288  ralrp  10374  facwordi  11304  rexuzre  11838  limsupgle  11953  ello12  11992  elo12  12003  lo1resb  12040  rlimresb  12041  o1resb  12042  isprm2  12768  isprm4  12770  acsfn2  13567  pgpfac1  15317  isirred2  15485  isdomn2  16042  ist1-2  17077  isnrm2  17088  dfcon2  17147  1stccn  17191  iskgen3  17246  hausdiag  17341  cnflf  17699  txflf  17703  cnfcf  17739  metcnp  18089  caucfil  18711  ovolgelb  18841  ismbl  18887  dyadmbllem  18956  itg2leub  19091  ellimc3  19231  mdegleb  19452  jensen  20285  dchrelbas2  20478  dchrelbas3  20479  nmoubi  21352  nmobndseqi  21359  nmobndseqiOLD  21360  h1dei  22131  nmopub  22490  nmfnleub  22507  mdsl1i  22903  mdsl2i  22904  elat2  22922  rmo3f  23180  rmo4fOLD  23181  climuzcnv  24006  axextprim  24049  biimpexp  24072  dfpo2  24114  dfon2lem8  24148  predreseq  24181  dffun10  24455  filnetlem4  26341  raldifsni  26764  dford4  27133  fnwe2lem2  27159  islindf4  27319  isdomn3  27534  pm11.62  27604  2sbc6g  27626  2rexsb  27959  2rexrsb  27960  rmoanim  27968  impexp3a  28331  dfvd2  28404  dfvd3  28416  bnj115  28824  bnj1109  28891  bnj1533  28957  bnj580  29018  bnj864  29027  bnj865  29028  bnj1049  29077  bnj1090  29082  bnj1093  29083  bnj1133  29092  bnj1171  29103  ax12conj2  29181  a12study8  29192  isat3  29570  isltrn2N  30382  cdlemefrs29bpre0  30658  cdleme32fva  30699
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