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

Theorem impexp 444
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 442 . 2  |-  ( ( ( ph  /\  ps )  ->  ch )  -> 
( ph  ->  ( ps 
->  ch ) ) )
2 pm3.31 443 . 2  |-  ( (
ph  ->  ( ps  ->  ch ) )  ->  (
( ph  /\  ps )  ->  ch ) )
31, 2impbii 188 1  |-  ( ( ( ph  /\  ps )  ->  ch )  <->  ( ph  ->  ( ps  ->  ch ) ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 369
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 185  df-an 371
This theorem is referenced by:  pm4.14  573  nan  575  pm4.87  579  imp4a  584  exp4a  601  imdistan  682  pm5.3  704  pm5.6  896  2sb6  2152  2sb6rfOLD  2164  2exsbOLD  2184  eu2OLD  2302  moanimOLD  2330  2eu6  2363  r2alf  2740  r3al  2763  r19.23t  2821  ceqsralt  2986  ralrab  3110  ralrab2  3114  euind  3135  reu2  3136  reu3  3138  rmo4  3141  reuind  3151  2reu5lem3  3155  rmo2  3271  rmo3  3273  ralss  3406  rabss  3417  raldifb  3484  raldifsni  3993  unissb  4111  elintrab  4128  ssintrab  4139  dftr5  4376  axrep5  4396  reusv2lem4  4484  reusv2  4486  reusv3  4488  raliunxp  4966  fununi  5472  dff13  5958  ordunisuc2  6444  dfom2  6467  dfsmo2  6794  qliftfun  7173  dfsup2  7680  wemapsolem  7752  iscard2  8134  acnnum  8210  aceq1  8275  dfac9  8293  dfacacn  8298  axgroth6  8982  sstskm  8996  infm3  10276  prime  10709  raluz  10890  raluz2  10891  nnwos  10909  ralrp  10996  facwordi  12048  rexuzre  12823  limsupgle  12938  ello12  12977  elo12  12988  lo1resb  13025  rlimresb  13026  o1resb  13027  isprm2  13753  isprm4  13755  acsfn2  14583  pgpfac1  16554  isirred2  16726  isdomn2  17292  islindf4  18108  ist1-2  18792  isnrm2  18803  dfcon2  18864  1stccn  18908  iskgen3  18963  hausdiag  19059  cnflf  19416  txflf  19420  cnfcf  19456  metcnp  19957  caucfil  20635  ovolgelb  20804  ismbl  20850  dyadmbllem  20920  itg2leub  21053  ellimc3  21195  mdegleb  21419  jensen  22266  dchrelbas2  22460  dchrelbas3  22461  nmoubi  23994  nmobndseqi  24001  nmobndseqiOLD  24002  h1dei  24775  nmopub  25134  nmfnleub  25151  mdsl1i  25547  mdsl2i  25548  elat2  25566  moel  25690  rmo3f  25702  rmo4fOLD  25703  eulerpartlemgvv  26606  climuzcnv  27162  axextprim  27198  biimpexp  27218  dfpo2  27411  dfon2lem8  27449  predreseq  27486  dffun10  27791  wl-2sb6d  28230  filnetlem4  28443  dford4  29220  fnwe2lem2  29246  isdomn3  29414  pm11.62  29489  2sbc6g  29511  2rexsb  29837  2rexrsb  29838  rmoanim  29846  modfsummod  30088  rabsssn  30560  snlindsntor  30711  exp3acom23g  30902  impexp3a  30916  dfvd2  30991  dfvd3  31003  bnj115  31413  bnj1109  31479  bnj1533  31544  bnj580  31605  bnj864  31614  bnj865  31615  bnj1049  31664  bnj1090  31669  bnj1093  31670  bnj1133  31679  bnj1171  31690  bj-axrep5  31930  isat3  32522  isltrn2N  33334  cdlemefrs29bpre0  33610  cdleme32fva  33651
  Copyright terms: Public domain W3C validator