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 578
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 577 . 2 ((𝜑 → (𝜓𝜒)) ↔ ((𝜑𝜓) ↔ (𝜑𝜒)))
31, 2mpbi 233 1 ((𝜑𝜓) ↔ (𝜑𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209  wa 399
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 210  df-an 400
This theorem is referenced by:  pm5.32ri  579  anbi2i  625  anabs5  662  abai  825  annotanannot  833  pm5.33  834  cases  1038  equsexvwOLD  2013  equsexv  2270  equsexALT  2442  2sb5rf  2497  2eu8  2744  eq2tri  2883  rexbiia  3234  reubiia  3375  rmobiia  3380  rabbiia  3449  ceqsrexbv  3627  euxfrw  3689  euxfr  3691  2reu5  3726  dfpss3  4039  eldifpr  4570  eldiftp  4597  eldifsn  4692  elrint  4890  elriin  4976  rabxp  5573  copsex2gb  5652  eliunxp  5681  dfres3  5831  restidsing  5895  ressn  6109  dflim2  6220  fncnv  6400  dff1o5  6597  respreima  6809  dff4  6840  dffo3  6841  f1ompt  6848  fsn  6870  fconst3  6949  fconst4  6950  eufnfv  6965  dff13  6987  f1mpt  6993  isocnv3  7059  isores2  7060  isoini  7065  eloprabga  7235  mpomptx  7239  resoprab  7244  elrnmpores  7262  ov6g  7287  dfwe2  7471  dflim3  7537  dflim4  7538  dfopab2  7725  dfoprab3s  7726  dfoprab3  7727  fparlem1  7782  fparlem2  7783  fsplit  7787  brtpos2  7873  dftpos3  7885  tpostpos  7887  dfsmo2  7959  dfrecs3  7984  tz7.48-1  8054  ondif1  8101  ondif2  8102  elixp2  8440  xpcomco  8582  eqinf  8924  infempty  8947  r0weon  9415  isinfcard  9495  dfac5lem1  9526  fpwwe  10045  axgroth6  10227  axgroth3  10230  elni2  10276  indpi  10306  recmulnq  10363  genpass  10408  lemul1a  11471  sup3  11575  elnn0z  11972  elznn0  11974  elznn  11975  eluz2b1  12297  eluz2b3  12300  elfz2nn0  12981  elfzo3  13037  shftidt2  14419  clim0  14842  fprod2dlem  15313  divalglem4  15724  ndvdsadd  15738  gcdaddmlem  15849  algfx  15901  isprm3  16004  isprm5  16028  isprm7  16029  xpsfrnel  16813  isacs2  16902  isfull2  17159  isfth2  17163  tosso  17624  odudlatb  17784  issubmndb  17948  nsgacs  18292  isgim2  18383  isabl2  18893  iscyg3  18983  iscrng2  19291  isdrng2  19487  drngprop  19488  issdrg2  19552  islmim2  19813  islpir2  19999  isnzr2  20011  iunocv  20800  ishil2  20838  islinds2  20932  ssntr  21641  isclo2  21671  isperf2  21735  isperf3  21736  nrmsep3  21938  isconn2  21997  iskgen3  22132  ptpjpre1  22154  tx1cn  22192  tx2cn  22193  hausdiag  22228  qustgplem  22704  istdrg2  22761  isngp2  23181  isngp3  23182  isnvc2  23283  isclmp  23680  iscvs  23710  isncvsngp  23732  ovoliunlem1  24084  ismbl2  24109  i1f1lem  24271  i1fres  24287  itg1climres  24296  pilem1  25024  ellogrn  25129  ellogdm  25208  1cubr  25406  atandm  25440  atandm2  25441  atandm3  25442  atandm4  25443  atans2  25495  eldmgm  25585  isfusgrcl  27089  nbgrel  27108  iscusgrvtx  27189  iscusgredg  27191  clwlkclwwlkflem  27767  isph  28583  h2hcau  28740  h2hlm  28741  issh2  28970  isch2  28984  h1dei  29311  elbdop2  29632  dfadj2  29646  cnvadj  29653  hhcno  29665  hhcnf  29666  eleigvec2  29719  riesz2  29827  rnbra  29868  elat2  30101  ofpreima  30396  mpomptxf  30411  f1od2  30443  maprnin  30453  xrofsup  30478  xrdifh  30489  cmpcref  31124  ofcfval  31364  ispisys2  31419  1stmbfm  31525  2ndmbfm  31526  eulerpartlems  31625  eulerpartlemgc  31627  eulerpartlemv  31629  eulerpartlemd  31631  eulerpartlemr  31639  eulerpartlemn  31646  ballotlemodife  31762  sgn3da  31806  oddprm2  31933  bnj945  32052  bnj1172  32280  bnj1296  32300  snmlval  32585  eldm3  33004  frr2  33152  madeval2  33297  brtxp2  33349  brpprod3a  33354  dffun10  33382  elfuns  33383  brimg  33405  dfrdg4  33419  ellines  33620  opnrebl  33675  bj-ax12ig  33976  bj-equsexval  34000  bj-csbsnlem  34236  bj-mpomptALT  34427  bj-elid6  34478  bj-eldiag  34484  bj-imdirid  34491  taupilem3  34616  topdifinffinlem  34644  relowlssretop  34660  wl-dfclab  34871  istotbnd3  35087  isbnd2  35099  isbnd3b  35101  exidcl  35192  isdrngo2  35274  isdrngo3  35275  iscrngo2  35313  isdmn2  35371  isfldidl2  35385  isdmn3  35390  brres2  35567  eldmqsres  35581  brxrn2  35665  islshpat  36191  iscvlat2N  36498  ishlat3N  36528  snatpsubN  36924  diclspsn  38368  prjspeclsp  39401  isnacs2  39442  islnm2  39817  islnr2  39853  islnr3  39854  isdomn3  39943  iscard5  40037  en2pr  40041  pren2  40047  elinintab  40070  elmapintab  40091  elinlem  40093  cnvcnvintabd  40095  k0004lem1  40632  dffo3f  41592  2reu8  43459  dfdfat2  43475  prproropf1olem0  43810  prprelb  43824  prprspr2  43826  isodd2  43945  iseven5  43974  isodd7  43975  oddprmne2  44025  ismhm0  44217  sgrp2sgrp  44280  0ringdif  44286  isrnghmmul  44309  eliunxp2  44527  mpomptx2  44528  elbigo  44756
  Copyright terms: Public domain W3C validator