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

Theorem impexp 435
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 433 . 2  |-  ( ( ( ph  /\  ps )  ->  ch )  -> 
( ph  ->  ( ps 
->  ch ) ) )
2 pm3.31 434 . 2  |-  ( (
ph  ->  ( ps  ->  ch ) )  ->  (
( ph  /\  ps )  ->  ch ) )
31, 2impbii 182 1  |-  ( ( ( ph  /\  ps )  ->  ch )  <->  ( ph  ->  ( ps  ->  ch ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 6    <-> wb 178    /\ wa 360
This theorem is referenced by:  pm4.14  564  nan  566  pm4.87  570  imp4a  575  exp4a  592  imdistan  673  pm5.3  695  pm5.6  883  exp3acom23g  1367  ax12b  1834  2sb6  2076  2sb6rf  2081  2exsb  2095  eu2  2143  moanim  2174  2eu6  2203  r2alf  2553  r3al  2575  r19.23t  2632  ceqsralt  2786  ralrab  2902  ralrab2  2906  euind  2927  reu2  2928  reu3  2930  rmo4  2933  reuind  2943  2reu5lem3  2947  rmo2  3051  rmo3  3053  ralss  3214  rabss  3225  unissb  3831  elintrab  3848  ssintrab  3859  dftr5  4090  axrep5  4110  reusv2lem4  4510  reusv2  4512  reusv3  4514  ordunisuc2  4607  dfom2  4630  raliunxp  4813  fununi  5254  dff13  5717  dfsmo2  6332  qliftfun  6711  dfsup2  7163  wemapso2lem  7233  iscard2  7577  acnnum  7647  aceq1  7712  dfac9  7730  dfacacn  7735  axgroth6  8418  sstskm  8432  infm3  9681  prime  10060  raluz  10235  raluz2  10236  nnwos  10254  ralrp  10340  facwordi  11269  rexuzre  11802  limsupgle  11917  ello12  11956  elo12  11967  lo1resb  12004  rlimresb  12005  o1resb  12006  isprm2  12729  isprm4  12731  acsfn2  13528  pgpfac1  15278  isirred2  15446  isdomn2  16003  ist1-2  17038  isnrm2  17049  dfcon2  17108  1stccn  17152  iskgen3  17207  hausdiag  17302  cnflf  17660  txflf  17664  cnfcf  17700  metcnp  18050  caucfil  18672  ovolgelb  18802  ismbl  18848  dyadmbllem  18917  itg2leub  19052  ellimc3  19192  mdegleb  19413  jensen  20246  dchrelbas2  20439  dchrelbas3  20440  nmoubi  21311  nmobndseqi  21318  nmobndseqiOLD  21319  h1dei  22090  nmopub  22449  nmfnleub  22466  mdsl1i  22862  mdsl2i  22863  elat2  22881  climuzcnv  23377  axextprim  23420  biimpexp  23443  dfpo2  23484  dfon2lem8  23516  predreseq  23549  filnetlem4  25698  raldifsni  26121  dford4  26490  fnwe2lem2  26516  islindf4  26676  isdomn3  26891  pm11.62  26961  2sbc6g  26984  2rexsb  27297  2rexrsb  27298  rmoanim  27306  impexp3a  27411  dfvd2  27484  dfvd3  27496  bnj115  27883  bnj1109  27950  bnj1533  28016  bnj580  28077  bnj864  28086  bnj865  28087  bnj1049  28136  bnj1090  28141  bnj1093  28142  bnj1133  28151  bnj1171  28162  ax12conj2  28358  a12study8  28369  isat3  28747  isltrn2N  29559  cdlemefrs29bpre0  29835  cdleme32fva  29876
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10
This theorem depends on definitions:  df-bi 179  df-an 362
  Copyright terms: Public domain W3C validator