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  903  2sb6  2150  2sb6rfOLD  2162  2exsbOLD  2183  eu2OLD  2307  moanimOLD  2333  2eu6OLD  2372  r2alf  2755  r3al  2778  r19.23t  2836  ceqsralt  3001  ralrab  3126  ralrab2  3130  euind  3151  reu2  3152  reu3  3154  rmo4  3157  reuind  3167  2reu5lem3  3171  rmo2  3288  rmo3  3290  ralss  3423  rabss  3434  raldifb  3501  raldifsni  4010  unissb  4128  elintrab  4145  ssintrab  4156  dftr5  4393  axrep5  4413  reusv2lem4  4501  reusv2  4503  reusv3  4505  raliunxp  4984  fununi  5489  dff13  5976  ordunisuc2  6460  dfom2  6483  dfsmo2  6813  qliftfun  7190  dfsup2  7697  wemapsolem  7769  iscard2  8151  acnnum  8227  aceq1  8292  dfac9  8310  dfacacn  8315  axgroth6  9000  sstskm  9014  infm3  10294  prime  10727  raluz  10908  raluz2  10909  nnwos  10927  ralrp  11014  facwordi  12070  rexuzre  12845  limsupgle  12960  ello12  12999  elo12  13010  lo1resb  13047  rlimresb  13048  o1resb  13049  isprm2  13776  isprm4  13778  acsfn2  14606  pgpfac1  16586  isirred2  16798  isdomn2  17376  evl1gsumd  17796  islindf4  18272  ist1-2  18956  isnrm2  18967  dfcon2  19028  1stccn  19072  iskgen3  19127  hausdiag  19223  cnflf  19580  txflf  19584  cnfcf  19620  metcnp  20121  caucfil  20799  ovolgelb  20968  ismbl  21014  dyadmbllem  21084  itg2leub  21217  ellimc3  21359  mdegleb  21540  jensen  22387  dchrelbas2  22581  dchrelbas3  22582  nmoubi  24177  nmobndseqi  24184  nmobndseqiOLD  24185  h1dei  24958  nmopub  25317  nmfnleub  25334  mdsl1i  25730  mdsl2i  25731  elat2  25749  moel  25872  rmo3f  25884  rmo4fOLD  25885  eulerpartlemgvv  26764  climuzcnv  27321  axextprim  27357  biimpexp  27377  dfpo2  27570  dfon2lem8  27608  predreseq  27645  dffun10  27950  wl-2sb6d  28389  filnetlem4  28607  dford4  29383  fnwe2lem2  29409  isdomn3  29577  pm11.62  29652  2sbc6g  29674  2rexsb  29999  2rexrsb  30000  rmoanim  30008  modfsummod  30250  rabsssn  30723  coe1fzgsumd  30843  snlindsntor  31010  expcomdg  31209  impexpd  31223  dfvd2  31297  dfvd3  31309  bnj115  31719  bnj1109  31785  bnj1533  31850  bnj580  31911  bnj864  31920  bnj865  31921  bnj1049  31970  bnj1090  31975  bnj1093  31976  bnj1133  31985  bnj1171  31996  bj-axrep5  32318  isat3  32957  isltrn2N  33769  cdlemefrs29bpre0  34045  cdleme32fva  34086
  Copyright terms: Public domain W3C validator