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

Theorem impexp 433
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 431 . 2  |-  ( ( ( ph  /\  ps )  ->  ch )  -> 
( ph  ->  ( ps 
->  ch ) ) )
2 pm3.31 432 . 2  |-  ( (
ph  ->  ( ps  ->  ch ) )  ->  (
( ph  /\  ps )  ->  ch ) )
31, 2impbii 180 1  |-  ( ( ( ph  /\  ps )  ->  ch )  <->  ( ph  ->  ( ps  ->  ch ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    /\ wa 358
This theorem is referenced by:  pm4.14  561  nan  563  pm4.87  567  imp4a  572  exp4a  589  imdistan  670  pm5.3  692  pm5.6  878  exp3acom23g  1361  ax12bOLD  1656  2sb6  2052  2sb6rf  2057  2exsb  2071  eu2  2168  moanim  2199  2eu6  2228  r2alf  2578  r3al  2600  r19.23t  2657  ceqsralt  2811  ralrab  2927  ralrab2  2931  euind  2952  reu2  2953  reu3  2955  rmo4  2958  reuind  2968  2reu5lem3  2972  rmo2  3076  rmo3  3078  ralss  3239  rabss  3250  unissb  3857  elintrab  3874  ssintrab  3885  dftr5  4116  axrep5  4136  reusv2lem4  4538  reusv2  4540  reusv3  4542  ordunisuc2  4635  dfom2  4658  raliunxp  4825  fununi  5316  dff13  5783  dfsmo2  6364  qliftfun  6743  dfsup2  7195  wemapso2lem  7265  iscard2  7609  acnnum  7679  aceq1  7744  dfac9  7762  dfacacn  7767  axgroth6  8450  sstskm  8464  infm3  9713  prime  10092  raluz  10267  raluz2  10268  nnwos  10286  ralrp  10372  facwordi  11302  rexuzre  11836  limsupgle  11951  ello12  11990  elo12  12001  lo1resb  12038  rlimresb  12039  o1resb  12040  isprm2  12766  isprm4  12768  acsfn2  13565  pgpfac1  15315  isirred2  15483  isdomn2  16040  ist1-2  17075  isnrm2  17086  dfcon2  17145  1stccn  17189  iskgen3  17244  hausdiag  17339  cnflf  17697  txflf  17701  cnfcf  17737  metcnp  18087  caucfil  18709  ovolgelb  18839  ismbl  18885  dyadmbllem  18954  itg2leub  19089  ellimc3  19229  mdegleb  19450  jensen  20283  dchrelbas2  20476  dchrelbas3  20477  nmoubi  21350  nmobndseqi  21357  nmobndseqiOLD  21358  h1dei  22129  nmopub  22488  nmfnleub  22505  mdsl1i  22901  mdsl2i  22902  elat2  22920  rmo3f  23178  rmo4fOLD  23179  climuzcnv  24004  axextprim  24047  biimpexp  24070  dfpo2  24112  dfon2lem8  24146  predreseq  24179  dffun10  24453  filnetlem4  26330  raldifsni  26753  dford4  27122  fnwe2lem2  27148  islindf4  27308  isdomn3  27523  pm11.62  27593  2sbc6g  27615  2rexsb  27948  2rexrsb  27949  rmoanim  27957  impexp3a  28275  dfvd2  28348  dfvd3  28360  bnj115  28751  bnj1109  28818  bnj1533  28884  bnj580  28945  bnj864  28954  bnj865  28955  bnj1049  29004  bnj1090  29009  bnj1093  29010  bnj1133  29019  bnj1171  29030  ax12conj2  29108  a12study8  29119  isat3  29497  isltrn2N  30309  cdlemefrs29bpre0  30585  cdleme32fva  30626
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 177  df-an 360
  Copyright terms: Public domain W3C validator