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 667
Description: Distribution of implication over biconditional (inference rule). (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 666 . 2 ((𝜑 → (𝜓𝜒)) ↔ ((𝜑𝜓) ↔ (𝜑𝜒)))
31, 2mpbi 219 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:  pm5.32ri  668  biadan2  672  anbi2i  726  abai  832  anabs5  847  pm5.33  918  cases  1004  equsexvw  1919  equsexv  2095  equsexALT  2282  2sb5rf  2439  2eu8  2548  eq2tri  2671  rexbiia  3022  reubiia  3104  rmobiia  3109  rabbiia  3161  ceqsrexbv  3307  euxfr  3359  2reu5  3383  dfpss3  3655  eldifpr  4152  eldiftp  4175  eldifsn  4260  elrint  4453  elriin  4529  reuxfrd  4819  opeqsn  4892  rabxp  5078  copsex2gb  5153  eliunxp  5181  restidsing  5377  ressn  5588  dflim2  5698  fncnv  5876  dff1o5  6059  respreima  6252  dff4  6281  dffo3  6282  f1ompt  6290  fsn  6308  fconst3  6382  fconst4  6383  eufnfv  6395  dff13  6416  f1mpt  6419  isocnv3  6482  isores2  6483  isoini  6488  eloprabga  6645  mpt2mptx  6649  resoprab  6654  elrnmpt2res  6672  ov6g  6696  dfwe2  6873  dflim3  6939  dflim4  6940  dfopab2  7113  dfoprab3s  7114  dfoprab3  7115  fparlem1  7164  fparlem2  7165  brtpos2  7245  dftpos3  7257  tpostpos  7259  dfsmo2  7331  dfrecs3  7356  tz7.48-1  7425  ondif1  7468  ondif2  7469  elixp2  7798  mapsnen  7920  xpcomco  7935  eqinf  8273  infempty  8295  r0weon  8718  isinfcard  8798  dfac5lem1  8829  fpwwe  9347  axgroth6  9529  axgroth3  9532  elni2  9578  indpi  9608  recmulnq  9665  genpass  9710  lemul1a  10756  sup3  10859  elnn0z  11267  elznn0  11269  elznn  11270  eluz2b1  11635  eluz2b3  11638  elfz2nn0  12300  elfzo3  12355  shftidt2  13669  clim0  14085  fprod2dlem  14549  divalglem4  14957  ndvdsadd  14972  gcdaddmlem  15083  algfx  15131  isprm3  15234  isprm5  15257  isprm7  15258  xpsfrnel  16046  isacs2  16137  isfull2  16394  isfth2  16398  tosso  16859  odudlatb  17019  nsgacs  17453  isgim2  17530  isabl2  18024  iscyg3  18111  iscrng2  18386  isdrng2  18580  drngprop  18581  islmim2  18887  islpir2  19072  isnzr2  19084  iunocv  19844  ishil2  19882  islinds2  19971  ssntr  20672  isclo2  20702  isperf2  20766  isperf3  20767  nrmsep3  20969  iscon2  21027  iskgen3  21162  ptpjpre1  21184  tx1cn  21222  tx2cn  21223  hausdiag  21258  qustgplem  21734  istdrg2  21791  isngp2  22211  isngp3  22212  isnvc2  22313  isclmp  22705  iscvs  22735  isncvsngp  22757  ovoliunlem1  23077  ismbl2  23102  i1f1lem  23262  i1fres  23278  itg1climres  23287  pilem1  24009  ellogrn  24110  ellogdm  24185  1cubr  24369  atandm  24403  atandm2  24404  atandm3  24405  atandm4  24406  atans2  24458  eldmgm  24548  isph  27061  h2hcau  27220  h2hlm  27221  issh2  27450  isch2  27464  h1dei  27793  elbdop2  28114  dfadj2  28128  cnvadj  28135  hhcno  28147  hhcnf  28148  eleigvec2  28201  riesz2  28309  rnbra  28350  elat2  28583  ofpreima  28848  mpt2mptxf  28860  f1od2  28887  maprnin  28894  xrofsup  28923  xrdifh  28932  cmpcref  29245  ofcfval  29487  ispisys2  29543  1stmbfm  29649  2ndmbfm  29650  eulerpartlems  29749  eulerpartlemgc  29751  eulerpartlemv  29753  eulerpartlemd  29755  eulerpartlemr  29763  eulerpartlemn  29770  ballotlemodife  29886  sgn3da  29930  bnj945  30098  bnj1172  30323  bnj1296  30343  snmlval  30567  dfres3  30902  eldm3  30905  nofulllem5  31105  brtxp2  31158  brpprod3a  31163  dffun10  31191  elfuns  31192  brimg  31214  dfrdg4  31228  ellines  31429  opnrebl  31485  bj-ax12ig  31802  bj-equsexval  31827  bj-csbsnlem  32090  bj-mpt2mptALT  32253  bj-elid3  32264  bj-eldiag  32268  taupilem3  32342  topdifinffinlem  32371  relowlssretop  32387  istotbnd3  32740  isbnd2  32752  isbnd3b  32754  exidcl  32845  isdrngo2  32927  isdrngo3  32928  iscrngo2  32966  isdmn2  33024  isfldidl2  33038  isdmn3  33043  islshpat  33322  iscvlat2N  33629  ishlat3N  33659  snatpsubN  34054  diclspsn  35501  isnacs2  36287  islnm2  36666  islnr2  36703  islnr3  36704  issdrg2  36787  isdomn3  36801  elinintab  36900  elmapintab  36921  elinlem  36923  cnvcnvintabd  36925  k0004lem1  37465  dffo3f  38359  2reu8  39841  dfdfat2  39860  isodd2  40086  iseven5  40114  isodd7  40115  oddprmne2  40162  isfusgrcl  40540  iscusgrvtx  40643  iscusgredg  40645  ismhm0  41595  sgrp2sgrp  41654  0ringdif  41660  isrnghmmul  41683  eliunxp2  41905  mpt2mptx2  41906  elbigo  42143
  Copyright terms: Public domain W3C validator