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

Theorem pm5.32i 637
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 636 . 2
31, 2mpbi 208 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 184  /\wa 369
This theorem is referenced by:  pm5.32ri  638  biadan2  642  anbi2i  694  abai  795  anabs5  809  pm5.33  878  cases  970  2sb5rf  2195  2eu8  2386  eq2tri  2525  rexbiia  2958  reubiia  3043  rmobiia  3048  rabbiia  3098  ceqsrexbv  3234  euxfr  3285  2reu5  3308  dfpss3  3589  eldifpr  4046  eldiftp  4072  eldifsn  4155  elrint  4328  elriin  4403  reuxfrd  4677  opeqsn  4748  dflim2  4939  rabxp  5041  copsex2gb  5118  eliunxp  5145  ressn  5548  fncnv  5657  dff1o5  5830  respreima  6016  dff4  6045  dffo3  6046  f1ompt  6053  fsn  6069  fconst3  6135  fconst4  6136  eufnfv  6146  dff13  6166  f1mpt  6169  isocnv3  6228  isores2  6229  isoini  6234  eloprabga  6389  mpt2mptx  6393  resoprab  6398  elrnmpt2res  6416  ov6g  6440  dfwe2  6617  dflim3  6682  dflim4  6683  dfopab2  6854  dfoprab3s  6855  dfoprab3  6856  fparlem1  6900  fparlem2  6901  brtpos2  6980  dftpos3  6992  tpostpos  6994  dfsmo2  7037  tz7.48-1  7127  ondif1  7170  ondif2  7171  elixp2  7493  mapsnen  7613  xpcomco  7627  r0weon  8411  isinfcard  8494  dfac5lem1  8525  fpwwe  9045  axgroth6  9227  axgroth3  9230  elni2  9276  indpi  9306  recmulnq  9363  genpass  9408  lemul1a  10421  sup3  10525  elnn0z  10902  elznn0  10904  elznn  10905  eluz2b1  11182  eluz2b3  11184  elfz2nn0  11798  elfzo3  11844  shftidt2  12914  clim0  13329  fprod2dlem  13784  divalglem4  14054  ndvdsadd  14066  gcdaddmlem  14166  algfx  14209  isprm3  14226  isprm5  14253  xpsfrnel  14960  isacs2  15050  isfull2  15280  isfth2  15284  tosso  15666  odudlatb  15826  nsgacs  16237  isgim2  16313  isabl2  16806  iscyg3  16889  iscrng2  17214  isdrng2  17406  drngprop  17407  islmim2  17712  islpir2  17899  isnzr2  17911  iunocv  18712  ishil2  18750  islinds2  18848  istps2OLD  19422  istps3OLD  19423  ssntr  19559  isclo2  19589  isperf2  19653  isperf3  19654  nrmsep3  19856  iscon2  19915  iskgen3  20050  ptpjpre1  20072  tx1cn  20110  tx2cn  20111  hausdiag  20146  qustgplem  20619  istdrg2  20680  isngp2  21117  isngp3  21118  isnvc2  21207  ovoliunlem1  21913  ismbl2  21938  i1f1lem  22096  i1fres  22112  itg1climres  22121  pilem1  22846  ellogrn  22947  ellogdm  23020  1cubr  23173  atandm  23207  atandm2  23208  atandm3  23209  atandm4  23210  atans2  23262  isgrpo2  25199  issubgo  25305  isph  25737  h2hcau  25896  h2hlm  25897  issh2  26126  isch2  26141  h1dei  26468  elbdop2  26790  dfadj2  26804  cnvadj  26811  hhcno  26823  hhcnf  26824  eleigvec2  26877  riesz2  26985  rnbra  27026  elat2  27259  ofpreima  27507  mpt2mptxf  27518  f1od2  27547  maprnin  27554  xrofsup  27582  xrdifh  27591  cmpcref  27853  ofcfval  28097  1stmbfm  28231  2ndmbfm  28232  eulerpartlems  28299  eulerpartlemgc  28301  eulerpartlemv  28303  eulerpartlemd  28305  eulerpartlemr  28313  eulerpartlemn  28320  ballotlemodife  28436  sgn3da  28480  eldmgm  28564  snmlval  28776  dfres3  29188  eldm3  29191  nofulllem5  29466  brtxp2  29531  brpprod3a  29536  dffun10  29564  elfuns  29565  brimg  29587  dfrdg4  29600  ellines  29802  dvtanlem  30064  opnrebl  30138  istotbnd3  30267  isbnd2  30279  isbnd3b  30281  exidcl  30338  isdrngo2  30361  isdrngo3  30362  iscrngo2  30395  isdmn2  30452  isfldidl2  30466  isdmn3  30471  isnacs2  30638  islnm2  31024  islnr2  31063  islnr3  31064  issdrg2  31147  isdomn3  31164  isprm7  31192  2reu8  32197  dfdfat2  32216  ismhm0  32493  sgrp2sgrp  32552  0ringdif  32676  isrnghmmul  32699  eliunxp2  32923  mpt2mptx2  32924  bnj945  33832  bnj1172  34057  bnj1296  34077  bj-csbsnlem  34470  bj-elid3  34601  bj-eldiag  34606  islshpat  34742  iscvlat2N  35049  ishlat3N  35079  snatpsubN  35474  diclspsn  36921  taupilem3  37694
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 185  df-an 371
  Copyright terms: Public domain W3C validator