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

Theorem impexp 461
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 459 . 2 (((𝜑𝜓) → 𝜒) → (𝜑 → (𝜓𝜒)))
2 pm3.31 460 . 2 ((𝜑 → (𝜓𝜒)) → ((𝜑𝜓) → 𝜒))
31, 2impbii 198 1 (((𝜑𝜓) → 𝜒) ↔ (𝜑 → (𝜓𝜒)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 195  wa 383
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 196  df-an 385
This theorem is referenced by:  pm4.14  600  nan  602  pm4.87  606  imp4aOLD  613  exp4aOLD  632  imdistan  721  pm5.3  744  pm5.6  949  2sb6  2432  r2allem  2921  r3al  2924  r19.23t  3003  ceqsralt  3202  ralrab  3335  ralrab2  3339  euind  3360  reu2  3361  reu3  3363  rmo4  3366  reuind  3378  2reu5lem3  3382  rmo2  3492  rmo3  3494  ralss  3631  rabss  3642  raldifb  3712  rabsssn  4162  raldifsni  4265  unissb  4405  elintrab  4423  ssintrab  4435  dftr5  4683  axrep5  4704  reusv2lem4  4798  reusv2  4800  reusv3  4802  raliunxp  5183  fununi  5878  fvn0ssdmfun  6258  dff13  6416  ordunisuc2  6936  dfom2  6959  dfsmo2  7331  qliftfun  7719  dfsup2  8233  wemapsolem  8338  iscard2  8685  acnnum  8758  aceq1  8823  dfac9  8841  dfacacn  8846  axgroth6  9529  sstskm  9543  infm3  10861  prime  11334  raluz  11612  raluz2  11613  nnwos  11631  ralrp  11728  facwordi  12938  cotr2g  13563  rexuzre  13940  limsupgle  14056  ello12  14095  elo12  14106  lo1resb  14143  rlimresb  14144  o1resb  14145  modfsummod  14367  isprm2  15233  isprm4  15235  isprm7  15258  acsfn2  16147  pgpfac1  18302  isirred2  18524  isdomn2  19120  coe1fzgsumd  19493  evl1gsumd  19542  islindf4  19996  ist1-2  20961  isnrm2  20972  dfcon2  21032  1stccn  21076  iskgen3  21162  hausdiag  21258  cnflf  21616  txflf  21620  cnfcf  21656  metcnp  22156  caucfil  22889  ovolgelb  23055  ismbl  23101  dyadmbllem  23173  itg2leub  23307  ellimc3  23449  mdegleb  23628  jensen  24515  dchrelbas2  24762  dchrelbas3  24763  nmoubi  27011  nmobndseqi  27018  nmobndseqiALT  27019  h1dei  27793  nmopub  28151  nmfnleub  28168  mdsl1i  28564  mdsl2i  28565  elat2  28583  moel  28707  rmo3f  28719  rmo4fOLD  28720  eulerpartlemgvv  29765  bnj115  30045  bnj1109  30111  bnj1533  30176  bnj580  30237  bnj864  30246  bnj865  30247  bnj1049  30296  bnj1090  30301  bnj1093  30302  bnj1133  30311  bnj1171  30322  climuzcnv  30819  axextprim  30832  biimpexp  30852  dfpo2  30898  dfon2lem8  30939  dffun10  31191  filnetlem4  31546  bj-axrep5  31980  wl-2sb6d  32520  poimirlem25  32604  poimirlem30  32609  isat3  33612  isltrn2N  34424  cdlemefrs29bpre0  34702  cdleme32fva  34743  dford4  36614  fnwe2lem2  36639  isdomn3  36801  ifpidg  36855  ifpim23g  36859  elmapintrab  36901  undmrnresiss  36929  df3or2  37079  df3an2  37080  dfhe3  37089  dffrege76  37253  dffrege115  37292  ntrneiiso  37409  pm11.62  37616  2sbc6g  37638  expcomdg  37727  impexpd  37740  dfvd2  37816  dfvd3  37828  rabssf  38334  2rexsb  39819  2rexrsb  39820  rmoanim  39828  snlindsntor  42054  elbigo2  42144
  Copyright terms: Public domain W3C validator