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

Theorem impexp 452
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 450 . 2 (((𝜑𝜓) → 𝜒) → (𝜑 → (𝜓𝜒)))
2 pm3.31 451 . 2 ((𝜑 → (𝜓𝜒)) → ((𝜑𝜓) → 𝜒))
31, 2impbii 208 1 (((𝜑𝜓) → 𝜒) ↔ (𝜑 → (𝜓𝜒)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 397
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 206  df-an 398
This theorem is referenced by:  imdistan  569  pm4.14  806  nan  829  pm4.87  842  pm5.6  1001  2sb6  2090  r2allem  3138  r3al  3192  r19.23t  3237  moelOLD  3377  ceqsralt  3475  rspc2gv  3588  ralrab  3650  ralrab2  3655  euind  3681  reu2  3682  reu3  3684  rmo4  3687  rmo3f  3691  reuind  3710  2reu5lem3  3714  rmo2  3842  rmo3  3844  rmoanim  3849  rmoanimALT  3850  ralss  4013  rabss  4028  raldifb  4103  rabsssn  4627  raldifsni  4754  unissb  4899  unissbOLD  4900  elintrab  4920  ssintrab  4931  dftr5  5225  dftr5OLD  5226  axrep5  5247  reusv2lem4  5355  reusv2  5357  reusv3  5359  raliunxp  5792  dfpo2  6245  fununi  6572  fvn0ssdmfun  7021  dff13  7197  ordunisuc2  7771  dfom2  7795  dfsmo2  8261  qliftfun  8675  dfsup2  9314  wemapsolem  9420  iscard2  9846  acnnum  9922  aceq1  9987  dfac9  10006  dfacacn  10011  axgroth6  10698  sstskm  10712  infm3  12048  prime  12515  raluz  12750  raluz2  12751  nnwos  12769  ralrp  12864  facwordi  14117  cotr2g  14795  rexuzre  15172  limsupgle  15294  ello12  15333  elo12  15344  lo1resb  15381  rlimresb  15382  o1resb  15383  modfsummod  15614  isprm2  16493  isprm4  16495  isprm7  16519  acsfn2  17478  pgpfac1  19788  isirred2  20053  isdomn2  20692  islindf4  21167  coe1fzgsumd  21595  evl1gsumd  21645  ist1-2  22620  isnrm2  22631  dfconn2  22692  1stccn  22736  iskgen3  22822  hausdiag  22918  cnflf  23275  txflf  23279  cnfcf  23315  metcnp  23819  caucfil  24569  ovolgelb  24766  ismbl  24812  dyadmbllem  24885  itg2leub  25021  ellimc3  25165  mdegleb  25351  jensen  26260  dchrelbas2  26507  dchrelbas3  26508  eqscut2  27067  nmoubi  29500  nmobndseqi  29507  nmobndseqiALT  29508  h1dei  30278  nmopub  30636  nmfnleub  30653  mdsl1i  31049  mdsl2i  31050  elat2  31068  islinds5  31937  eulerpartlemgvv  32737  bnj115  33098  bnj1109  33159  bnj1533  33225  bnj580  33286  bnj864  33295  bnj865  33296  bnj1049  33347  bnj1090  33352  bnj1093  33353  bnj1133  33362  bnj1171  33373  climuzcnv  34022  axextprim  34035  biimpexp  34051  dfon2lem8  34143  frpoins3xpg  34163  frpoins3xp3g  34164  xpord2ind  34170  xpord3ind  34176  dffun10  34385  filnetlem4  34739  bj-substax12  35072  wl-2sb6d  35899  poimirlem25  35989  poimirlem30  35994  ralin  36592  r2alan  36593  inxpss  36658  moantr  36711  isat3  37655  isltrn2N  38469  cdlemefrs29bpre0  38745  cdleme32fva  38786  sn-axrep5v  40523  dford4  41187  fnwe2lem2  41212  isdomn3  41365  ifpidg  41494  ifpim23g  41498  elmapintrab  41579  undmrnresiss  41607  df3or2  41771  df3an2  41772  dfhe3  41778  dffrege76  41942  dffrege115  41981  ntrneiiso  42096  ismnushort  42314  pm11.62  42407  2sbc6g  42428  expcomdg  42515  impexpd  42528  dfvd2  42594  dfvd3  42606  rabssf  43062  2rexsb  45051  2rexrsb  45052  snlindsntor  46270  elbigo2  46356  exp12bd  46599  ralbidb  46603  ralbidc  46604
  Copyright terms: Public domain W3C validator