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  4400  elintrab  4418  ssintrab  4430  dftr5  4678  axrep5  4699  reusv2lem4  4793  reusv2  4795  reusv3  4797  raliunxp  5171  fununi  5864  fvn0ssdmfun  6243  dff13  6394  ordunisuc2  6914  dfom2  6937  dfsmo2  7309  qliftfun  7697  dfsup2  8211  wemapsolem  8316  iscard2  8663  acnnum  8736  aceq1  8801  dfac9  8819  dfacacn  8824  axgroth6  9507  sstskm  9521  infm3  10834  prime  11293  raluz  11571  raluz2  11572  nnwos  11590  ralrp  11687  facwordi  12896  cotr2g  13512  rexuzre  13889  limsupgle  14005  ello12  14044  elo12  14055  lo1resb  14092  rlimresb  14093  o1resb  14094  modfsummod  14316  isprm2  15182  isprm4  15184  isprm7  15207  acsfn2  16096  pgpfac1  18251  isirred2  18473  isdomn2  19069  coe1fzgsumd  19442  evl1gsumd  19491  islindf4  19944  ist1-2  20909  isnrm2  20920  dfcon2  20980  1stccn  21024  iskgen3  21110  hausdiag  21206  cnflf  21564  txflf  21568  cnfcf  21604  metcnp  22104  caucfil  22834  ovolgelb  23000  ismbl  23046  dyadmbllem  23118  itg2leub  23252  ellimc3  23394  mdegleb  23573  jensen  24460  dchrelbas2  24707  dchrelbas3  24708  nmoubi  26805  nmobndseqi  26812  nmobndseqiALT  26813  h1dei  27587  nmopub  27945  nmfnleub  27962  mdsl1i  28358  mdsl2i  28359  elat2  28377  moel  28501  rmo3f  28513  rmo4fOLD  28514  eulerpartlemgvv  29559  bnj115  29839  bnj1109  29905  bnj1533  29970  bnj580  30031  bnj864  30040  bnj865  30041  bnj1049  30090  bnj1090  30095  bnj1093  30096  bnj1133  30105  bnj1171  30116  climuzcnv  30613  axextprim  30626  biimpexp  30646  dfpo2  30692  dfon2lem8  30733  dffun10  30985  filnetlem4  31340  bj-axrep5  31774  wl-2sb6d  32314  poimirlem25  32398  poimirlem30  32403  isat3  33406  isltrn2N  34218  cdlemefrs29bpre0  34496  cdleme32fva  34537  dford4  36408  fnwe2lem2  36433  isdomn3  36595  ifpidg  36649  ifpim23g  36653  elmapintrab  36695  undmrnresiss  36723  df3or2  36873  df3an2  36874  dfhe3  36883  dffrege76  37047  dffrege115  37086  ntrneiiso  37203  pm11.62  37410  2sbc6g  37432  expcomdg  37521  impexpd  37534  dfvd2  37610  dfvd3  37622  rabssf  38128  2rexsb  39613  2rexrsb  39614  rmoanim  39622  snlindsntor  42046  elbigo2  42136
  Copyright terms: Public domain W3C validator