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

Theorem pm5.32i 576
Description: Distribution of implication over biconditional (inference form). (Contributed by NM, 1-Aug-1994.)
Hypothesis
Ref Expression
pm5.32i.1 (𝜑 → (𝜓𝜒))
Assertion
Ref Expression
pm5.32i ((𝜑𝜓) ↔ (𝜑𝜒))

Proof of Theorem pm5.32i
StepHypRef Expression
1 pm5.32i.1 . 2 (𝜑 → (𝜓𝜒))
2 pm5.32 575 . 2 ((𝜑 → (𝜓𝜒)) ↔ ((𝜑𝜓) ↔ (𝜑𝜒)))
31, 2mpbi 229 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:  pm5.32ri  577  anbi2i  624  anabs5  661  abai  825  annotanannot  833  pm5.33  834  cases  1041  equsexALT  2417  2sb5rf  2470  2eu8  2658  eq2tri  2803  rexbiia  3092  reubiia  3336  rmobiia  3342  rabbiia  3414  ceqsrexbv  3591  euxfrw  3661  euxfr  3663  2reu5  3698  dfpss3  4027  eldifpr  4597  eldiftp  4626  eldifsn  4726  elrint  4929  elriin  5017  rabxp  5646  copsex2gb  5728  eliunxp  5759  dfres3  5908  restidsing  5972  ressn  6203  dflim2  6337  fncnv  6536  dff1o5  6755  respreima  6975  dff4  7009  dffo3  7010  f1ompt  7017  fsn  7039  fconst3  7121  fconst4  7122  eufnfv  7137  dff13  7160  f1mpt  7166  isocnv3  7235  isores2  7236  isoini  7241  eloprabga  7414  eloprabgaOLD  7415  mpomptx  7419  resoprab  7424  elrnmpores  7443  ov6g  7468  dfwe2  7656  dflim3  7726  dflim4  7727  dfopab2  7924  dfoprab3s  7925  dfoprab3  7926  fparlem1  7984  fparlem2  7985  fsplit  7989  brtpos2  8079  dftpos3  8091  tpostpos  8093  dfsmo2  8209  dfrecs3  8234  dfrecs3OLD  8235  tz7.48-1  8305  ondif1  8362  ondif2  8363  elixp2  8720  xpcomco  8887  pssnn  8989  enfi  9011  eqinf  9287  infempty  9310  ttrclselem2  9528  frr2  9562  r0weon  9814  isinfcard  9894  dfac5lem1  9925  fpwwe  10448  axgroth6  10630  axgroth3  10633  elni2  10679  indpi  10709  recmulnq  10766  genpass  10811  lemul1a  11875  sup3  11978  elnn0z  12378  elznn0  12380  elznn  12381  eluz2b1  12705  eluz2b3  12708  elfz2nn0  13393  elfzo3  13450  shftidt2  14837  clim0  15260  fprod2dlem  15735  divalglem4  16150  ndvdsadd  16164  gcdaddmlem  16276  algfx  16330  isprm3  16433  isprm5  16457  isprm7  16458  xpsfrnel  17318  isacs2  17407  isfull2  17672  isfth2  17676  tosso  18182  odudlatb  18288  issubmndb  18489  nsgacs  18835  isgim2  18926  isabl2  19440  iscyg3  19531  iscrng2  19847  isdrng2  20046  drngprop  20047  issdrg2  20111  islmim2  20373  islpir2  20567  isnzr2  20579  iunocv  20931  ishil2  20971  islinds2  21065  ssntr  22254  isclo2  22284  isperf2  22348  isperf3  22349  nrmsep3  22551  isconn2  22610  iskgen3  22745  ptpjpre1  22767  tx1cn  22805  tx2cn  22806  hausdiag  22841  qustgplem  23317  istdrg2  23374  isngp2  23798  isngp3  23799  isnvc2  23908  isclmp  24305  iscvs  24335  isncvsngp  24358  ovoliunlem1  24711  ismbl2  24736  i1f1lem  24898  i1fres  24915  itg1climres  24924  pilem1  25655  ellogrn  25760  ellogdm  25839  1cubr  26037  atandm  26071  atandm2  26072  atandm3  26073  atandm4  26074  atans2  26126  eldmgm  26216  isfusgrcl  27733  nbgrel  27752  iscusgrvtx  27833  iscusgredg  27835  clwlkclwwlkflem  28413  isph  29229  h2hcau  29386  h2hlm  29387  issh2  29616  isch2  29630  h1dei  29957  elbdop2  30278  dfadj2  30292  cnvadj  30299  hhcno  30311  hhcnf  30312  eleigvec2  30365  riesz2  30473  rnbra  30514  elat2  30747  ofpreima  31047  mpomptxf  31061  f1od2  31101  maprnin  31111  xrofsup  31135  xrdifh  31146  prmidl0  31671  cmpcref  31845  ofcfval  32111  ispisys2  32166  1stmbfm  32272  2ndmbfm  32273  eulerpartlems  32372  eulerpartlemgc  32374  eulerpartlemv  32376  eulerpartlemd  32378  eulerpartlemr  32386  eulerpartlemn  32393  ballotlemodife  32509  sgn3da  32553  oddprm2  32680  bnj945  32798  bnj1172  33026  bnj1296  33046  snmlval  33338  eldm3  33773  madeval2  34082  brtxp2  34228  brpprod3a  34233  dffun10  34261  elfuns  34262  brimg  34284  dfrdg4  34298  ellines  34499  opnrebl  34554  bj-ax12ig  34862  bj-equsexval  34886  bj-substw  34949  bj-csbsnlem  35132  bj-clel3gALT  35265  bj-mpomptALT  35334  bj-elid6  35385  bj-eldiag  35391  bj-imdiridlem  35400  bj-imdirco  35405  bj-isrvec  35509  taupilem3  35534  topdifinffinlem  35562  relowlssretop  35578  wl-dfclab  35791  istotbnd3  35973  isbnd2  35985  isbnd3b  35987  exidcl  36078  isdrngo2  36160  isdrngo3  36161  iscrngo2  36199  isdmn2  36257  isfldidl2  36271  isdmn3  36276  brres2  36450  eldmqsres  36464  brxrn2  36547  islshpat  37073  iscvlat2N  37380  ishlat3N  37410  snatpsubN  37806  diclspsn  39250  prjspeclsp  40488  isnacs2  40565  islnm2  40941  islnr2  40977  islnr3  40978  isdomn3  41067  minregex  41179  iscard5  41181  en2pr  41192  pren2  41198  elinintab  41221  elmapintab  41242  elinlem  41244  cnvcnvintabd  41246  sqrtcvallem1  41277  reabsifneg  41278  reabsifpos  41280  k0004lem1  41795  dffo3f  42761  2reu8  44662  dfdfat2  44678  prproropf1olem0  45012  prprelb  45026  prprspr2  45028  isodd2  45145  iseven5  45174  isodd7  45175  oddprmne2  45225  ismhm0  45417  sgrp2sgrp  45480  0ringdif  45486  isrnghmmul  45509  eliunxp2  45727  mpomptx2  45728  elbigo  45955  opndisj  46254  isnrm4  46282  iscnrm3  46304  iscnrm4  46306  catprs  46350
  Copyright terms: Public domain W3C validator