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  1657  2sb6  2055  2sb6rf  2060  2exsb  2074  eu2  2169  moanim  2200  2eu6  2229  r2alf  2579  r3al  2601  r19.23t  2658  ceqsralt  2812  ralrab  2928  ralrab2  2932  euind  2953  reu2  2954  reu3  2956  rmo4  2959  reuind  2969  2reu5lem3  2973  rmo2  3077  rmo3  3079  ralss  3240  rabss  3251  unissb  3858  elintrab  3875  ssintrab  3886  dftr5  4117  axrep5  4137  reusv2lem4  4537  reusv2  4539  reusv3  4541  ordunisuc2  4634  dfom2  4657  raliunxp  4824  fununi  5282  dff13  5745  dfsmo2  6360  qliftfun  6739  dfsup2  7191  wemapso2lem  7261  iscard2  7605  acnnum  7675  aceq1  7740  dfac9  7758  dfacacn  7763  axgroth6  8446  sstskm  8460  infm3  9709  prime  10088  raluz  10263  raluz2  10264  nnwos  10282  ralrp  10368  facwordi  11298  rexuzre  11832  limsupgle  11947  ello12  11986  elo12  11997  lo1resb  12034  rlimresb  12035  o1resb  12036  isprm2  12762  isprm4  12764  acsfn2  13561  pgpfac1  15311  isirred2  15479  isdomn2  16036  ist1-2  17071  isnrm2  17082  dfcon2  17141  1stccn  17185  iskgen3  17240  hausdiag  17335  cnflf  17693  txflf  17697  cnfcf  17733  metcnp  18083  caucfil  18705  ovolgelb  18835  ismbl  18881  dyadmbllem  18950  itg2leub  19085  ellimc3  19225  mdegleb  19446  jensen  20279  dchrelbas2  20472  dchrelbas3  20473  nmoubi  21344  nmobndseqi  21351  nmobndseqiOLD  21352  h1dei  22125  nmopub  22484  nmfnleub  22501  mdsl1i  22897  mdsl2i  22898  elat2  22916  climuzcnv  23411  axextprim  23454  biimpexp  23477  dfpo2  23518  dfon2lem8  23550  predreseq  23583  filnetlem4  25741  raldifsni  26164  dford4  26533  fnwe2lem2  26559  islindf4  26719  isdomn3  26934  pm11.62  27004  2sbc6g  27026  2rexsb  27339  2rexrsb  27340  rmoanim  27348  impexp3a  27558  dfvd2  27631  dfvd3  27643  bnj115  28030  bnj1109  28097  bnj1533  28163  bnj580  28224  bnj864  28233  bnj865  28234  bnj1049  28283  bnj1090  28288  bnj1093  28289  bnj1133  28298  bnj1171  28309  ax12conj2  28387  a12study8  28398  isat3  28776  isltrn2N  29588  cdlemefrs29bpre0  29864  cdleme32fva  29905
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