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  2sb6  2073  2sb6rf  2078  2exsb  2091  eu2  2138  moanim  2169  2eu6  2198  r2alf  2540  r3al  2562  r19.23t  2619  ceqsralt  2749  ralrab  2864  ralrab2  2868  euind  2889  reu2  2892  reu3  2894  rmo4  2897  reuind  2903  rmo3  3006  ralss  3160  rabss  3171  unissb  3755  elintrab  3772  ssintrab  3783  disjiun  3910  dftr5  4013  axrep5  4033  reusv2lem4  4429  reusv2  4431  reusv3  4433  ordunisuc2  4526  dfom2  4549  raliunxp  4732  fununi  5173  dff13  5635  dfsmo2  6250  qliftfun  6629  dfsup2  7079  wemapso2lem  7149  iscard2  7493  acnnum  7563  aceq1  7628  dfac9  7646  dfacacn  7651  axgroth6  8330  sstskm  8344  infm3  9593  prime  9971  raluz  10146  raluz2  10147  nnwos  10165  ralrp  10251  facwordi  11180  rexuzre  11713  limsupgle  11828  ello12  11867  elo12  11878  lo1resb  11915  rlimresb  11916  o1resb  11917  isprm2  12640  isprm4  12642  acsfn2  13409  pgpfac1  15150  isirred2  15318  isdomn2  15872  ist1-2  16907  isnrm2  16918  dfcon2  16977  1stccn  17021  iskgen3  17076  hausdiag  17171  cnflf  17529  txflf  17533  cnfcf  17569  metcnp  17919  caucfil  18541  ovolgelb  18671  ismbl  18717  dyadmbllem  18786  itg2leub  18921  ellimc3  19061  mdegleb  19282  jensen  20115  dchrelbas2  20308  dchrelbas3  20309  nmoubi  21180  nmobndseqi  21187  nmobndseqiOLD  21188  h1dei  21959  nmopub  22318  nmfnleub  22335  mdsl1i  22731  mdsl2i  22732  elat2  22750  climuzcnv  23175  axextprim  23218  biimpexp  23241  dfpo2  23282  dfon2lem8  23314  predreseq  23347  filnetlem4  25496  raldifsni  25919  dford4  26288  fnwe2lem2  26314  islindf4  26474  isdomn3  26689  pm11.62  26759  2sbc6g  26782  impexp3a  26968  dfvd2  27041  dfvd3  27053  bnj115  27440  bnj1109  27507  bnj1533  27573  bnj580  27634  bnj864  27643  bnj865  27644  bnj1049  27693  bnj1090  27698  bnj1093  27699  bnj1133  27708  bnj1171  27719  ax12conj2  27797  a12study8  27808  isat3  28186  isltrn2N  28998  cdlemefrs29bpre0  29274  cdleme32fva  29315
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