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

Theorem impexp 452
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 450 . 2  |-  ( ( ( ph  /\  ps )  ->  ch )  -> 
( ph  ->  ( ps 
->  ch ) ) )
2 pm3.31 451 . 2  |-  ( (
ph  ->  ( ps  ->  ch ) )  ->  (
( ph  /\  ps )  ->  ch ) )
31, 2impbii 192 1  |-  ( ( ( ph  /\  ps )  ->  ch )  <->  ( ph  ->  ( ps  ->  ch ) ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 189    /\ wa 375
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 190  df-an 377
This theorem is referenced by:  pm4.14  586  nan  588  pm4.87  592  imp4a  598  exp4a  615  imdistan  700  pm5.3  723  pm5.6  928  2sb6  2284  r2allem  2775  r2alfOLD  2777  r3al  2780  r3alOLD  2838  r19.23t  2877  ceqsralt  3083  ralrab  3212  ralrab2  3216  euind  3237  reu2  3238  reu3  3240  rmo4  3243  reuind  3255  2reu5lem3  3259  rmo2  3368  rmo3  3370  ralss  3507  rabss  3518  raldifb  3585  rabsssn  4014  raldifsni  4115  unissb  4243  elintrab  4260  ssintrab  4272  dftr5  4514  axrep5  4534  reusv2lem4  4621  reusv2  4623  reusv3  4625  raliunxp  4993  fununi  5671  fvn0ssdmfun  6036  dff13  6184  ordunisuc2  6698  dfom2  6721  dfsmo2  7092  qliftfun  7474  dfsup2  7984  wemapsolem  8091  iscard2  8436  acnnum  8509  aceq1  8574  dfac9  8592  dfacacn  8597  axgroth6  9279  sstskm  9293  infm3  10596  prime  11045  raluz  11236  raluz2  11237  nnwos  11255  ralrp  11350  facwordi  12506  cotr2g  13089  rexuzre  13464  limsupgle  13584  ello12  13629  elo12  13640  lo1resb  13677  rlimresb  13678  o1resb  13679  modfsummod  13903  isprm2  14681  isprm4  14683  acsfn2  15618  pgpfac1  17762  isirred2  17978  isdomn2  18572  coe1fzgsumd  18945  evl1gsumd  18994  islindf4  19445  ist1-2  20412  isnrm2  20423  dfcon2  20483  1stccn  20527  iskgen3  20613  hausdiag  20709  cnflf  21066  txflf  21070  cnfcf  21106  metcnp  21605  caucfil  22302  ovolgelb  22482  ismbl  22529  dyadmbllem  22606  itg2leub  22741  ellimc3  22883  mdegleb  23062  jensen  23963  dchrelbas2  24214  dchrelbas3  24215  nmoubi  26462  nmobndseqi  26469  nmobndseqiALT  26470  h1dei  27252  nmopub  27610  nmfnleub  27627  mdsl1i  28023  mdsl2i  28024  elat2  28042  moel  28168  rmo3f  28180  rmo4fOLD  28181  eulerpartlemgvv  29258  bnj115  29580  bnj1109  29647  bnj1533  29712  bnj580  29773  bnj864  29782  bnj865  29783  bnj1049  29832  bnj1090  29837  bnj1093  29838  bnj1133  29847  bnj1171  29858  climuzcnv  30364  axextprim  30377  biimpexp  30397  dfpo2  30444  dfon2lem8  30485  dffun10  30730  filnetlem4  31086  bj-axrep5  31452  wl-2sb6d  31933  poimirlem25  32010  poimirlem30  32015  isat3  32918  isltrn2N  33730  cdlemefrs29bpre0  34008  cdleme32fva  34049  dford4  35929  fnwe2lem2  35954  isdomn3  36126  ifpidg  36180  ifpim23g  36184  elmapintrab  36227  undmrnresiss  36255  df3or2  36405  df3an2  36406  dfhe3  36415  dffrege76  36580  dffrege115  36619  isprm7  36704  pm11.62  36788  2sbc6g  36810  expcomdg  36900  impexpd  36914  dfvd2  36992  dfvd3  37004  2rexsb  38629  2rexrsb  38630  rmoanim  38638  snlindsntor  40537  elbigo2  40636
  Copyright terms: Public domain W3C validator