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

Theorem impexp 434
Description: Import-export theorem. Part of Theorem *4.87 of [WhiteheadRussell] p. 122. (Contributed by NM, 5-Aug-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 432 . 2  |-  ( ( ( ph  /\  ps )  ->  ch )  -> 
( ph  ->  ( ps 
->  ch ) ) )
2 pm3.31 433 . 2  |-  ( (
ph  ->  ( ps  ->  ch ) )  ->  (
( ph  /\  ps )  ->  ch ) )
31, 2impbii 181 1  |-  ( ( ( ph  /\  ps )  ->  ch )  <->  ( ph  ->  ( ps  ->  ch ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    /\ wa 359
This theorem is referenced by:  pm4.14  562  nan  564  pm4.87  568  imp4a  573  exp4a  590  imdistan  671  pm5.3  693  pm5.6  879  exp3acom23g  1377  ax12bOLD  1698  2sb6  2162  2sb6rf  2168  2exsb  2182  eu2  2279  moanim  2310  2eu6  2339  r2alf  2701  r3al  2723  r19.23t  2780  ceqsralt  2939  ralrab  3056  ralrab2  3060  euind  3081  reu2  3082  reu3  3084  rmo4  3087  reuind  3097  2reu5lem3  3101  rmo2  3206  rmo3  3208  ralss  3369  rabss  3380  raldifb  3447  unissb  4005  elintrab  4022  ssintrab  4033  dftr5  4265  axrep5  4285  reusv2lem4  4686  reusv2  4688  reusv3  4690  ordunisuc2  4783  dfom2  4806  raliunxp  4973  fununi  5476  dff13  5963  dfsmo2  6568  qliftfun  6948  dfsup2  7405  wemapso2lem  7475  iscard2  7819  acnnum  7889  aceq1  7954  dfac9  7972  dfacacn  7977  axgroth6  8659  sstskm  8673  infm3  9923  prime  10306  raluz  10481  raluz2  10482  nnwos  10500  ralrp  10586  facwordi  11535  rexuzre  12111  limsupgle  12226  ello12  12265  elo12  12276  lo1resb  12313  rlimresb  12314  o1resb  12315  isprm2  13042  isprm4  13044  acsfn2  13843  pgpfac1  15593  isirred2  15761  isdomn2  16314  ist1-2  17365  isnrm2  17376  dfcon2  17435  1stccn  17479  iskgen3  17534  hausdiag  17630  cnflf  17987  txflf  17991  cnfcf  18027  metcnp  18524  caucfil  19189  ovolgelb  19329  ismbl  19375  dyadmbllem  19444  itg2leub  19579  ellimc3  19719  mdegleb  19940  jensen  20780  dchrelbas2  20974  dchrelbas3  20975  nmoubi  22226  nmobndseqi  22233  nmobndseqiOLD  22234  h1dei  23005  nmopub  23364  nmfnleub  23381  mdsl1i  23777  mdsl2i  23778  elat2  23796  rmo3f  23935  rmo4fOLD  23936  climuzcnv  25061  axextprim  25103  biimpexp  25126  dfpo2  25326  dfon2lem8  25360  predreseq  25393  dffun10  25667  filnetlem4  26300  raldifsni  26624  dford4  26990  fnwe2lem2  27016  islindf4  27176  isdomn3  27391  pm11.62  27461  2sbc6g  27483  2rexsb  27815  2rexrsb  27816  rmoanim  27824  impexp3a  28307  dfvd2  28380  dfvd3  28392  bnj115  28796  bnj1109  28863  bnj1533  28929  bnj580  28990  bnj864  28999  bnj865  29000  bnj1049  29049  bnj1090  29054  bnj1093  29055  bnj1133  29064  bnj1171  29075  2sb6NEW7  29311  2sb6rfOLD7  29447  2exsbOLD7  29452  isat3  29790  isltrn2N  30602  cdlemefrs29bpre0  30878  cdleme32fva  30919
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 178  df-an 361
  Copyright terms: Public domain W3C validator