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

Theorem impexp 447
Description: Import-export theorem. Part of Theorem *4.87 of [WhiteheadRussell] p. 122. (Contributed by NM, 10-Jan-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 445 . 2  |-  ( ( ( ph  /\  ps )  ->  ch )  -> 
( ph  ->  ( ps 
->  ch ) ) )
2 pm3.31 446 . 2  |-  ( (
ph  ->  ( ps  ->  ch ) )  ->  (
( ph  /\  ps )  ->  ch ) )
31, 2impbii 190 1  |-  ( ( ( ph  /\  ps )  ->  ch )  <->  ( ph  ->  ( ps  ->  ch ) ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 187    /\ wa 370
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 188  df-an 372
This theorem is referenced by:  pm4.14  580  nan  582  pm4.87  586  imp4a  592  exp4a  609  imdistan  693  pm5.3  716  pm5.6  920  2sb6  2240  2eu6OLD  2362  r2allem  2807  r2alfOLD  2809  r3al  2812  r3alOLD  2870  r19.23t  2910  ceqsralt  3111  ralrab  3239  ralrab2  3243  euind  3264  reu2  3265  reu3  3267  rmo4  3270  reuind  3281  2reu5lem3  3285  rmo2  3394  rmo3  3396  ralss  3533  rabss  3544  raldifb  3611  raldifsni  4133  unissb  4253  elintrab  4270  ssintrab  4282  dftr5  4523  axrep5  4543  reusv2lem4  4629  reusv2  4631  reusv3  4633  raliunxp  4994  fununi  5667  fvn0ssdmfun  6028  dff13  6174  ordunisuc2  6685  dfom2  6708  dfsmo2  7074  qliftfun  7456  dfsup2  7964  wemapsolem  8065  iscard2  8409  acnnum  8481  aceq1  8546  dfac9  8564  dfacacn  8569  axgroth6  9252  sstskm  9266  infm3  10568  prime  11016  raluz  11207  raluz2  11208  nnwos  11226  ralrp  11321  facwordi  12471  cotr2g  13019  rexuzre  13394  limsupgle  13513  ello12  13558  elo12  13569  lo1resb  13606  rlimresb  13607  o1resb  13608  modfsummod  13832  isprm2  14603  isprm4  14605  acsfn2  15520  pgpfac1  17648  isirred2  17864  isdomn2  18458  coe1fzgsumd  18831  evl1gsumd  18880  islindf4  19327  ist1-2  20294  isnrm2  20305  dfcon2  20365  1stccn  20409  iskgen3  20495  hausdiag  20591  cnflf  20948  txflf  20952  cnfcf  20988  metcnp  21487  caucfil  22146  ovolgelb  22311  ismbl  22357  dyadmbllem  22434  itg2leub  22569  ellimc3  22711  mdegleb  22890  jensen  23779  dchrelbas2  24028  dchrelbas3  24029  nmoubi  26258  nmobndseqi  26265  nmobndseqiALT  26266  h1dei  27038  nmopub  27396  nmfnleub  27413  mdsl1i  27809  mdsl2i  27810  elat2  27828  moel  27954  rmo3f  27966  rmo4fOLD  27967  eulerpartlemgvv  29035  bnj115  29319  bnj1109  29386  bnj1533  29451  bnj580  29512  bnj864  29521  bnj865  29522  bnj1049  29571  bnj1090  29576  bnj1093  29577  bnj1133  29586  bnj1171  29597  climuzcnv  30103  axextprim  30116  biimpexp  30136  dfpo2  30182  dfon2lem8  30223  dffun10  30466  filnetlem4  30822  bj-axrep5  31158  wl-2sb6d  31595  poimirlem25  31669  poimirlem30  31674  isat3  32582  isltrn2N  33394  cdlemefrs29bpre0  33672  cdleme32fva  33713  dford4  35590  fnwe2lem2  35615  isdomn3  35780  ifpidg  35834  ifpim23g  35838  dfhe3  36007  dffrege76  36172  dffrege115  36211  isprm7  36297  pm11.62  36381  2sbc6g  36403  expcomdg  36493  impexpd  36507  dfvd2  36587  dfvd3  36599  2rexsb  37991  2rexrsb  37992  rmoanim  38000  rabsssn  38881  snlindsntor  39033  elbigo2  39133
  Copyright terms: Public domain W3C validator