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

Theorem impexp 448
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 446 . 2  |-  ( ( ( ph  /\  ps )  ->  ch )  -> 
( ph  ->  ( ps 
->  ch ) ) )
2 pm3.31 447 . 2  |-  ( (
ph  ->  ( ps  ->  ch ) )  ->  (
( ph  /\  ps )  ->  ch ) )
31, 2impbii 191 1  |-  ( ( ( ph  /\  ps )  ->  ch )  <->  ( ph  ->  ( ps  ->  ch ) ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 188    /\ wa 371
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 189  df-an 373
This theorem is referenced by:  pm4.14  581  nan  583  pm4.87  587  imp4a  593  exp4a  610  imdistan  694  pm5.3  717  pm5.6  921  2sb6  2244  r2allem  2802  r2alfOLD  2804  r3al  2807  r3alOLD  2865  r19.23t  2905  ceqsralt  3111  ralrab  3238  ralrab2  3242  euind  3263  reu2  3264  reu3  3266  rmo4  3269  reuind  3281  2reu5lem3  3285  rmo2  3394  rmo3  3396  ralss  3533  rabss  3544  raldifb  3611  raldifsni  4136  unissb  4256  elintrab  4273  ssintrab  4285  dftr5  4527  axrep5  4547  reusv2lem4  4634  reusv2  4636  reusv3  4638  raliunxp  4999  fununi  5673  fvn0ssdmfun  6034  dff13  6180  ordunisuc2  6691  dfom2  6714  dfsmo2  7083  qliftfun  7465  dfsup2  7973  wemapsolem  8080  iscard2  8424  acnnum  8496  aceq1  8561  dfac9  8579  dfacacn  8584  axgroth6  9266  sstskm  9280  infm3  10581  prime  11029  raluz  11220  raluz2  11221  nnwos  11239  ralrp  11334  facwordi  12486  cotr2g  13046  rexuzre  13421  limsupgle  13540  ello12  13585  elo12  13596  lo1resb  13633  rlimresb  13634  o1resb  13635  modfsummod  13859  isprm2  14637  isprm4  14639  acsfn2  15574  pgpfac1  17718  isirred2  17934  isdomn2  18528  coe1fzgsumd  18901  evl1gsumd  18950  islindf4  19400  ist1-2  20367  isnrm2  20378  dfcon2  20438  1stccn  20482  iskgen3  20568  hausdiag  20664  cnflf  21021  txflf  21025  cnfcf  21061  metcnp  21560  caucfil  22257  ovolgelb  22437  ismbl  22484  dyadmbllem  22561  itg2leub  22696  ellimc3  22838  mdegleb  23017  jensen  23918  dchrelbas2  24169  dchrelbas3  24170  nmoubi  26417  nmobndseqi  26424  nmobndseqiALT  26425  h1dei  27207  nmopub  27565  nmfnleub  27582  mdsl1i  27978  mdsl2i  27979  elat2  27997  moel  28123  rmo3f  28135  rmo4fOLD  28136  eulerpartlemgvv  29223  bnj115  29545  bnj1109  29612  bnj1533  29677  bnj580  29738  bnj864  29747  bnj865  29748  bnj1049  29797  bnj1090  29802  bnj1093  29803  bnj1133  29812  bnj1171  29823  climuzcnv  30329  axextprim  30342  biimpexp  30362  dfpo2  30408  dfon2lem8  30449  dffun10  30692  filnetlem4  31048  bj-axrep5  31383  wl-2sb6d  31858  poimirlem25  31935  poimirlem30  31940  isat3  32848  isltrn2N  33660  cdlemefrs29bpre0  33938  cdleme32fva  33979  dford4  35860  fnwe2lem2  35885  isdomn3  36057  ifpidg  36111  ifpim23g  36115  elmapintrab  36158  undmrnresiss  36186  df3or2  36336  df3an2  36337  dfhe3  36346  dffrege76  36511  dffrege115  36550  isprm7  36636  pm11.62  36720  2sbc6g  36742  expcomdg  36832  impexpd  36846  dfvd2  36926  dfvd3  36938  2rexsb  38468  2rexrsb  38469  rmoanim  38477  rabsssn  39731  snlindsntor  39883  elbigo2  39982
  Copyright terms: Public domain W3C validator