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

Theorem impexp 451
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 449 . 2 (((𝜑𝜓) → 𝜒) → (𝜑 → (𝜓𝜒)))
2 pm3.31 450 . 2 ((𝜑 → (𝜓𝜒)) → ((𝜑𝜓) → 𝜒))
31, 2impbii 210 1 (((𝜑𝜓) → 𝜒) ↔ (𝜑 → (𝜓𝜒)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207  wa 396
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 208  df-an 397
This theorem is referenced by:  imdistan  568  pm4.14  803  nan  825  pm4.87  837  pm5.6  995  2sb6  2085  r2allem  3200  r3al  3202  r19.23t  3313  ceqsralt  3529  rspc2gv  3631  ralrab  3684  ralrab2  3689  euind  3714  reu2  3715  reu3  3717  rmo4  3720  rmo3f  3724  reuind  3743  2reu5lem3  3747  rmo2  3869  rmo3  3871  rmo3OLD  3872  rmoanim  3877  rmoanimALT  3878  ralss  4036  rabss  4047  raldifb  4120  rabsssn  4599  raldifsni  4722  unissb  4863  elintrab  4881  ssintrab  4892  dftr5  5167  axrep5  5188  reusv2lem4  5293  reusv2  5295  reusv3  5297  raliunxp  5704  fununi  6423  fvn0ssdmfun  6835  dff13  7004  ordunisuc2  7547  dfom2  7570  dfsmo2  7975  qliftfun  8372  dfsup2  8897  wemapsolem  9003  iscard2  9394  acnnum  9467  aceq1  9532  dfac9  9551  dfacacn  9556  axgroth6  10239  sstskm  10253  infm3  11589  prime  12052  raluz  12285  raluz2  12286  nnwos  12304  ralrp  12399  facwordi  13639  cotr2g  14326  rexuzre  14702  limsupgle  14824  ello12  14863  elo12  14874  lo1resb  14911  rlimresb  14912  o1resb  14913  modfsummod  15139  isprm2  16016  isprm4  16018  isprm7  16042  acsfn2  16924  pgpfac1  19133  isirred2  19382  isdomn2  20002  coe1fzgsumd  20400  evl1gsumd  20450  islindf4  20912  ist1-2  21885  isnrm2  21896  dfconn2  21957  1stccn  22001  iskgen3  22087  hausdiag  22183  cnflf  22540  txflf  22544  cnfcf  22580  metcnp  23080  caucfil  23815  ovolgelb  24010  ismbl  24056  dyadmbllem  24129  itg2leub  24264  ellimc3  24406  mdegleb  24587  jensen  25494  dchrelbas2  25741  dchrelbas3  25742  nmoubi  28477  nmobndseqi  28484  nmobndseqiALT  28485  h1dei  29255  nmopub  29613  nmfnleub  29630  mdsl1i  30026  mdsl2i  30027  elat2  30045  moel  30180  islinds5  30860  eulerpartlemgvv  31534  bnj115  31895  bnj1109  31958  bnj1533  32024  bnj580  32085  bnj864  32094  bnj865  32095  bnj1049  32144  bnj1090  32149  bnj1093  32150  bnj1133  32159  bnj1171  32170  climuzcnv  32812  axextprim  32825  biimpexp  32844  dfpo2  32889  dfon2lem8  32933  dffun10  33273  filnetlem4  33627  wl-2sb6d  34676  wl-dfrmosb  34735  wl-dfrmov  34736  wl-dfrmof  34737  poimirlem25  34799  poimirlem30  34804  inxpss  35452  moantr  35499  isat3  36325  isltrn2N  37138  cdlemefrs29bpre0  37414  cdleme32fva  37455  sn-axrep5v  38988  dford4  39506  fnwe2lem2  39531  isdomn3  39684  ifpidg  39737  ifpim23g  39741  elmapintrab  39816  undmrnresiss  39844  df3or2  39993  df3an2  39994  dfhe3  40001  dffrege76  40165  dffrege115  40204  ntrneiiso  40321  pm11.62  40606  2sbc6g  40627  expcomdg  40714  impexpd  40727  dfvd2  40793  dfvd3  40805  rabssf  41266  2rexsb  43180  2rexrsb  43181  snlindsntor  44424  elbigo2  44510
  Copyright terms: Public domain W3C validator