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  2eu6OLD  2368  r2allem  2816  r2alfOLD  2818  r3al  2821  r3alOLD  2879  r19.23t  2919  ceqsralt  3117  ralrab  3245  ralrab2  3249  euind  3270  reu2  3271  reu3  3273  rmo4  3276  reuind  3287  2reu5lem3  3291  rmo2  3410  rmo3  3412  ralss  3548  rabss  3559  raldifb  3626  raldifsni  4141  unissb  4262  elintrab  4279  ssintrab  4291  dftr5  4529  axrep5  4549  reusv2lem4  4637  reusv2  4639  reusv3  4641  raliunxp  5128  fununi  5640  fvn0ssdmfun  6003  dff13  6147  ordunisuc2  6660  dfom2  6683  dfsmo2  7016  qliftfun  7394  dfsup2  7900  wemapsolem  7973  iscard2  8355  acnnum  8431  aceq1  8496  dfac9  8514  dfacacn  8519  axgroth6  9204  sstskm  9218  infm3  10503  prime  10944  raluz  11133  raluz2  11134  nnwos  11153  ralrp  11242  facwordi  12341  rexuzre  13159  limsupgle  13274  ello12  13313  elo12  13324  lo1resb  13361  rlimresb  13362  o1resb  13363  modfsummod  13582  isprm2  14097  isprm4  14099  acsfn2  14932  pgpfac1  16999  isirred2  17218  isdomn2  17816  coe1fzgsumd  18212  evl1gsumd  18261  islindf4  18740  ist1-2  19714  isnrm2  19725  dfcon2  19786  1stccn  19830  iskgen3  19916  hausdiag  20012  cnflf  20369  txflf  20373  cnfcf  20409  metcnp  20910  caucfil  21588  ovolgelb  21757  ismbl  21803  dyadmbllem  21874  itg2leub  22007  ellimc3  22149  mdegleb  22330  jensen  23183  dchrelbas2  23377  dchrelbas3  23378  nmoubi  25552  nmobndseqi  25559  nmobndseqiOLD  25560  h1dei  26333  nmopub  26692  nmfnleub  26709  mdsl1i  27105  mdsl2i  27106  elat2  27124  moel  27247  rmo3f  27259  rmo4fOLD  27260  eulerpartlemgvv  28181  climuzcnv  28903  axextprim  28939  biimpexp  28959  dfpo2  29152  dfon2lem8  29190  predreseq  29227  dffun10  29532  wl-2sb6d  29976  filnetlem4  30167  dford4  30939  fnwe2lem2  30965  isdomn3  31133  isprm7  31161  pm11.62  31247  2sbc6g  31269  2rexsb  32009  2rexrsb  32010  rmoanim  32018  rabsssn  32628  snlindsntor  32782  expcomdg  32977  impexpd  32991  dfvd2  33064  dfvd3  33076  bnj115  33486  bnj1109  33552  bnj1533  33617  bnj580  33678  bnj864  33687  bnj865  33688  bnj1049  33737  bnj1090  33742  bnj1093  33743  bnj1133  33752  bnj1171  33763  bj-axrep5  34090  isat3  34734  isltrn2N  35546  cdlemefrs29bpre0  35824  cdleme32fva  35865  cotr2g  37441
  Copyright terms: Public domain W3C validator