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

Theorem impexp 454
Description: Import-export theorem. Part of Theorem *4.87 of [WhiteheadRussell] p. 122. (Contributed by NM, 10-Jan-1993.) (Proof shortened by Wolf Lammen, 24-Mar-2013.)
Assertion
Ref Expression
impexp (((𝜑𝜓) → 𝜒) ↔ (𝜑 → (𝜓𝜒)))

Proof of Theorem impexp
StepHypRef Expression
1 pm3.3 452 . 2 (((𝜑𝜓) → 𝜒) → (𝜑 → (𝜓𝜒)))
2 pm3.31 453 . 2 ((𝜑 → (𝜓𝜒)) → ((𝜑𝜓) → 𝜒))
31, 2impbii 212 1 (((𝜑𝜓) → 𝜒) ↔ (𝜑 → (𝜓𝜒)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209  wa 399
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 210  df-an 400
This theorem is referenced by:  imdistan  571  pm4.14  806  nan  828  pm4.87  840  pm5.6  999  2sb6  2095  r2allem  3194  r3al  3196  r19.23t  3305  ceqsralt  3513  rspc2gv  3617  ralrab  3670  ralrab2  3675  euind  3700  reu2  3701  reu3  3703  rmo4  3706  rmo3f  3710  reuind  3729  2reu5lem3  3733  rmo2  3853  rmo3  3855  rmoanim  3860  rmoanimALT  3861  ralss  4021  rabss  4032  raldifb  4105  rabsssn  4590  raldifsni  4711  unissb  4853  elintrab  4871  ssintrab  4882  dftr5  5158  axrep5  5179  reusv2lem4  5285  reusv2  5287  reusv3  5289  raliunxp  5693  fununi  6412  fvn0ssdmfun  6825  dff13  6997  ordunisuc2  7544  dfom2  7567  dfsmo2  7969  qliftfun  8367  dfsup2  8894  wemapsolem  9000  iscard2  9391  acnnum  9465  aceq1  9530  dfac9  9549  dfacacn  9554  axgroth6  10237  sstskm  10251  infm3  11587  prime  12051  raluz  12284  raluz2  12285  nnwos  12303  ralrp  12397  facwordi  13645  cotr2g  14327  rexuzre  14703  limsupgle  14825  ello12  14864  elo12  14875  lo1resb  14912  rlimresb  14913  o1resb  14914  modfsummod  15140  isprm2  16015  isprm4  16017  isprm7  16041  acsfn2  16925  pgpfac1  19193  isirred2  19442  isdomn2  20060  coe1fzgsumd  20458  evl1gsumd  20508  islindf4  20970  ist1-2  21943  isnrm2  21954  dfconn2  22015  1stccn  22059  iskgen3  22145  hausdiag  22241  cnflf  22598  txflf  22602  cnfcf  22638  metcnp  23139  caucfil  23878  ovolgelb  24075  ismbl  24121  dyadmbllem  24194  itg2leub  24329  ellimc3  24473  mdegleb  24656  jensen  25565  dchrelbas2  25812  dchrelbas3  25813  nmoubi  28546  nmobndseqi  28553  nmobndseqiALT  28554  h1dei  29324  nmopub  29682  nmfnleub  29699  mdsl1i  30095  mdsl2i  30096  elat2  30114  moel  30249  islinds5  30952  eulerpartlemgvv  31654  bnj115  32015  bnj1109  32078  bnj1533  32144  bnj580  32205  bnj864  32214  bnj865  32215  bnj1049  32266  bnj1090  32271  bnj1093  32272  bnj1133  32281  bnj1171  32292  climuzcnv  32934  axextprim  32947  biimpexp  32966  dfpo2  33011  dfon2lem8  33055  dffun10  33395  filnetlem4  33749  bj-subst  34075  wl-2sb6d  34864  wl-dfrmosb  34923  wl-dfrmov  34924  wl-dfrmof  34925  poimirlem25  34987  poimirlem30  34992  inxpss  35634  moantr  35681  isat3  36508  isltrn2N  37321  cdlemefrs29bpre0  37597  cdleme32fva  37638  sn-axrep5v  39274  dford4  39817  fnwe2lem2  39842  isdomn3  39995  ifpidg  40046  ifpim23g  40050  elmapintrab  40123  undmrnresiss  40151  df3or2  40316  df3an2  40317  dfhe3  40324  dffrege76  40488  dffrege115  40527  ntrneiiso  40644  pm11.62  40949  2sbc6g  40970  expcomdg  41057  impexpd  41070  dfvd2  41136  dfvd3  41148  rabssf  41607  2rexsb  43513  2rexrsb  43514  snlindsntor  44736  elbigo2  44822
  Copyright terms: Public domain W3C validator