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

Theorem impexp 444
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 442 . 2  |-  ( ( ( ph  /\  ps )  ->  ch )  -> 
( ph  ->  ( ps 
->  ch ) ) )
2 pm3.31 443 . 2  |-  ( (
ph  ->  ( ps  ->  ch ) )  ->  (
( ph  /\  ps )  ->  ch ) )
31, 2impbii 188 1  |-  ( ( ( ph  /\  ps )  ->  ch )  <->  ( ph  ->  ( ps  ->  ch ) ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 367
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 185  df-an 369
This theorem is referenced by:  pm4.14  576  nan  578  pm4.87  582  imp4a  587  exp4a  604  imdistan  687  pm5.3  709  pm5.6  910  2sb6  2190  2eu6OLD  2381  r2allem  2829  r2alfOLD  2831  r3al  2834  r3alOLD  2892  r19.23t  2932  ceqsralt  3130  ralrab  3258  ralrab2  3262  euind  3283  reu2  3284  reu3  3286  rmo4  3289  reuind  3300  2reu5lem3  3304  rmo2  3413  rmo3  3415  ralss  3552  rabss  3563  raldifb  3630  raldifsni  4146  unissb  4266  elintrab  4283  ssintrab  4295  dftr5  4535  axrep5  4555  reusv2lem4  4641  reusv2  4643  reusv3  4645  raliunxp  5131  fununi  5636  fvn0ssdmfun  5998  dff13  6141  ordunisuc2  6652  dfom2  6675  dfsmo2  7010  qliftfun  7388  dfsup2  7894  wemapsolem  7967  iscard2  8348  acnnum  8424  aceq1  8489  dfac9  8507  dfacacn  8512  axgroth6  9195  sstskm  9209  infm3  10497  prime  10939  raluz  11130  raluz2  11131  nnwos  11150  ralrp  11240  facwordi  12349  cotr2g  12894  rexuzre  13267  limsupgle  13382  ello12  13421  elo12  13432  lo1resb  13469  rlimresb  13470  o1resb  13471  modfsummod  13690  isprm2  14309  isprm4  14311  acsfn2  15152  pgpfac1  17326  isirred2  17545  isdomn2  18143  coe1fzgsumd  18539  evl1gsumd  18588  islindf4  19040  ist1-2  20015  isnrm2  20026  dfcon2  20086  1stccn  20130  iskgen3  20216  hausdiag  20312  cnflf  20669  txflf  20673  cnfcf  20709  metcnp  21210  caucfil  21888  ovolgelb  22057  ismbl  22103  dyadmbllem  22174  itg2leub  22307  ellimc3  22449  mdegleb  22630  jensen  23516  dchrelbas2  23710  dchrelbas3  23711  nmoubi  25885  nmobndseqi  25892  nmobndseqiALT  25893  h1dei  26666  nmopub  27025  nmfnleub  27042  mdsl1i  27438  mdsl2i  27439  elat2  27457  moel  27580  rmo3f  27592  rmo4fOLD  27593  eulerpartlemgvv  28579  climuzcnv  29301  axextprim  29314  biimpexp  29334  dfpo2  29425  dfon2lem8  29462  predreseq  29499  dffun10  29792  wl-2sb6d  30248  filnetlem4  30439  dford4  31210  fnwe2lem2  31236  isdomn3  31405  isprm7  31433  pm11.62  31541  2sbc6g  31563  2rexsb  32414  2rexrsb  32415  rmoanim  32423  rabsssn  33174  snlindsntor  33326  elbigo2  33427  expcomdg  33656  impexpd  33670  dfvd2  33750  dfvd3  33762  bnj115  34179  bnj1109  34246  bnj1533  34311  bnj580  34372  bnj864  34381  bnj865  34382  bnj1049  34431  bnj1090  34436  bnj1093  34437  bnj1133  34446  bnj1171  34457  bj-axrep5  34779  isat3  35429  isltrn2N  36241  cdlemefrs29bpre0  36519  cdleme32fva  36560  ifpidg  38105  ifpim23g  38112  dfhe3  38249  lem1frege76a  38417
  Copyright terms: Public domain W3C validator