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

Theorem impexp 446
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 444 . 2  |-  ( ( ( ph  /\  ps )  ->  ch )  -> 
( ph  ->  ( ps 
->  ch ) ) )
2 pm3.31 445 . 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 369
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 371
This theorem is referenced by:  pm4.14  578  nan  580  pm4.87  584  imp4a  589  exp4a  606  imdistan  689  pm5.3  711  pm5.6  910  2sb6  2172  2sb6rfOLD  2184  2exsbOLD  2205  eu2OLD  2329  moanimOLD  2355  2eu6OLD  2394  r2allem  2839  r2alfOLD  2841  r3al  2844  r3alOLD  2902  r19.23t  2941  ceqsralt  3137  ralrab  3265  ralrab2  3269  euind  3290  reu2  3291  reu3  3293  rmo4  3296  reuind  3307  2reu5lem3  3311  rmo2  3428  rmo3  3430  ralss  3566  rabss  3577  raldifb  3644  raldifsni  4157  unissb  4277  elintrab  4294  ssintrab  4305  dftr5  4543  axrep5  4563  reusv2lem4  4651  reusv2  4653  reusv3  4655  raliunxp  5140  fununi  5652  dff13  6152  ordunisuc2  6657  dfom2  6680  dfsmo2  7015  qliftfun  7393  dfsup2  7898  wemapsolem  7971  iscard2  8353  acnnum  8429  aceq1  8494  dfac9  8512  dfacacn  8517  axgroth6  9202  sstskm  9216  infm3  10498  prime  10937  raluz  11125  raluz2  11126  nnwos  11145  ralrp  11234  facwordi  12331  rexuzre  13144  limsupgle  13259  ello12  13298  elo12  13309  lo1resb  13346  rlimresb  13347  o1resb  13348  modfsummod  13567  isprm2  14080  isprm4  14082  acsfn2  14914  pgpfac1  16921  isirred2  17134  isdomn2  17719  coe1fzgsumd  18115  evl1gsumd  18164  islindf4  18640  ist1-2  19614  isnrm2  19625  dfcon2  19686  1stccn  19730  iskgen3  19785  hausdiag  19881  cnflf  20238  txflf  20242  cnfcf  20278  metcnp  20779  caucfil  21457  ovolgelb  21626  ismbl  21672  dyadmbllem  21743  itg2leub  21876  ellimc3  22018  mdegleb  22199  jensen  23046  dchrelbas2  23240  dchrelbas3  23241  nmoubi  25363  nmobndseqi  25370  nmobndseqiOLD  25371  h1dei  26144  nmopub  26503  nmfnleub  26520  mdsl1i  26916  mdsl2i  26917  elat2  26935  moel  27058  rmo3f  27070  rmo4fOLD  27071  eulerpartlemgvv  27955  climuzcnv  28512  axextprim  28548  biimpexp  28568  dfpo2  28761  dfon2lem8  28799  predreseq  28836  dffun10  29141  wl-2sb6d  29585  filnetlem4  29802  dford4  30575  fnwe2lem2  30601  isdomn3  30769  isprm7  30795  pm11.62  30878  2sbc6g  30900  2rexsb  31642  2rexrsb  31643  rmoanim  31651  rabsssn  31984  snlindsntor  32145  expcomdg  32348  impexpd  32362  dfvd2  32436  dfvd3  32448  bnj115  32858  bnj1109  32924  bnj1533  32989  bnj580  33050  bnj864  33059  bnj865  33060  bnj1049  33109  bnj1090  33114  bnj1093  33115  bnj1133  33124  bnj1171  33135  bj-axrep5  33459  isat3  34104  isltrn2N  34916  cdlemefrs29bpre0  35192  cdleme32fva  35233
  Copyright terms: Public domain W3C validator