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  19789  isirred2  20054  isdomn2  20693  islindf4  21168  coe1fzgsumd  21596  evl1gsumd  21646  ist1-2  22621  isnrm2  22632  dfconn2  22693  1stccn  22737  iskgen3  22823  hausdiag  22919  cnflf  23276  txflf  23280  cnfcf  23316  metcnp  23820  caucfil  24570  ovolgelb  24767  ismbl  24813  dyadmbllem  24886  itg2leub  25022  ellimc3  25166  mdegleb  25352  jensen  26261  dchrelbas2  26508  dchrelbas3  26509  eqscut2  27068  nmoubi  29513  nmobndseqi  29520  nmobndseqiALT  29521  h1dei  30291  nmopub  30649  nmfnleub  30666  mdsl1i  31062  mdsl2i  31063  elat2  31081  islinds5  31950  eulerpartlemgvv  32750  bnj115  33111  bnj1109  33172  bnj1533  33238  bnj580  33299  bnj864  33308  bnj865  33309  bnj1049  33360  bnj1090  33365  bnj1093  33366  bnj1133  33375  bnj1171  33386  climuzcnv  34035  axextprim  34048  biimpexp  34064  dfon2lem8  34156  frpoins3xpg  34176  frpoins3xp3g  34177  xpord2ind  34183  xpord3ind  34189  dffun10  34395  filnetlem4  34749  bj-substax12  35082  wl-2sb6d  35909  poimirlem25  35999  poimirlem30  36004  ralin  36602  r2alan  36603  inxpss  36668  moantr  36721  isat3  37665  isltrn2N  38479  cdlemefrs29bpre0  38755  cdleme32fva  38796  sn-axrep5v  40533  dford4  41219  fnwe2lem2  41244  isdomn3  41397  ifpidg  41526  ifpim23g  41530  elmapintrab  41611  undmrnresiss  41639  df3or2  41803  df3an2  41804  dfhe3  41810  dffrege76  41974  dffrege115  42013  ntrneiiso  42128  ismnushort  42346  pm11.62  42439  2sbc6g  42460  expcomdg  42547  impexpd  42560  dfvd2  42626  dfvd3  42638  rabssf  43094  2rexsb  45083  2rexrsb  45084  snlindsntor  46302  elbigo2  46388  exp12bd  46631  ralbidb  46635  ralbidc  46636
  Copyright terms: Public domain W3C validator