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

Theorem bicomd 213
Description: Commute two sides of a biconditional in a deduction. (Contributed by NM, 14-May-1993.)
Hypothesis
Ref Expression
bicomd.1 (𝜑 → (𝜓𝜒))
Assertion
Ref Expression
bicomd (𝜑 → (𝜒𝜓))

Proof of Theorem bicomd
StepHypRef Expression
1 bicomd.1 . 2 (𝜑 → (𝜓𝜒))
2 bicom 212 . 2 ((𝜓𝜒) ↔ (𝜒𝜓))
31, 2sylib 208 1 (𝜑 → (𝜒𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196
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 197
This theorem is referenced by:  impbid2  216  syl5ibr  236  ibir  257  bitr2d  269  bitr3d  270  bitr4d  271  syl5rbb  273  syl6rbb  277  con1bid  344  pm5.5  350  imnot  354  anabs5  886  pm5.55  975  annotanannot  977  pm5.54  981  baibr  983  rbaib  985  baibd  986  rbaibd  987  ninba  1003  pm5.75  1016  sbequ12r  2247  cbvalv  2406  sbal1  2585  euor2  2640  abbi1dv  2869  necon3bbid  2957  necon4bbid  2961  ralcom2  3230  gencbvex  3378  sbhypf  3381  alexeqg  3459  clel2g  3466  clel3g  3468  reu8  3531  sbceq2a  3576  sbcco2  3588  reu8nf  3645  raltpd  4446  ssdifsn  4451  disjxun  4790  opabid  5120  soeq2  5195  posn  5332  xpiindi  5401  fvopab6  6461  cbvfo  6695  f1eqcocnv  6707  isoid  6730  isoini  6739  isosolem  6748  riotaeqimp  6785  resoprab2  6910  tfisi  7211  tfinds2  7216  f1oweALT  7305  dfoprab3  7379  opiota  7384  mpt2curryd  7552  oalimcl  7797  omword  7807  oeword  7827  nnacan  7865  nnmcan  7871  findcard2s  8354  funisfsupp  8433  suppeqfsuppbi  8442  eqinf  8543  inflb  8548  infglb  8549  infglbb  8550  infltoreq  8561  infempty  8565  brwdomn0  8627  cantnfp1lem3  8738  ssrankr1  8859  r1pw  8869  aleph11  9068  alephval3  9094  gch-kn  9662  wunex2  9723  lttri2  10283  wloglei  10723  divne0b  10859  lemul1  11038  nnnle0  11214  div4p1lem1div2  11450  nn0ind-raph  11640  zindd  11641  suprfinzcl  11655  rebtwnz  11951  qreccl  11972  xrlttri2  12139  2resupmax  12183  xmulneg1  12263  iooshf  12416  difreicc  12468  fzofzim  12680  elfzomelpfzo  12737  elfznelfzo  12738  divfl0  12790  zmodid2  12863  2submod  12896  modfzo0difsn  12907  om2uzlti  12914  expcan  13078  hashvnfin  13314  hashneq0  13318  prhash2ex  13350  hashgt0elex  13352  hashgt12el  13373  hashgt12el2  13374  hashbclem  13399  hashf1lem2  13403  prprrab  13418  swrdn0  13601  swrd0  13605  2swrdeqwrdeq  13624  swrdswrd  13631  swrdccat3  13663  repswswrd  13702  cshf1  13727  cshw1repsw  13740  relexpindlem  13973  absz  14221  iserex  14557  prodrb  14832  absdvdsb  15173  dvdsabsb  15174  modmulconst  15186  dvdsadd  15197  dvdsabseq  15208  mod2eq0even  15243  oddnn02np1  15245  oddge22np1  15246  evennn02n  15247  evennn2n  15248  zeo5  15253  sadadd2lem2  15345  smupvallem  15378  gcdass  15437  lcmdvds  15494  lcmass  15500  divgcdcoprm0  15552  divgcdcoprmex  15553  1nprm  15565  dvdsnprmd  15576  ncoprmlnprm  15609  isevengcd2  15611  m1dvdsndvds  15676  cshws0  15981  sbcie2s  16089  sbcie3s  16090  dfiso2  16604  initoid  16827  termoid  16828  funcestrcsetclem8  16959  lublecllem  17160  odudlatb  17368  issubm2  17520  mgm2nsgrplem2  17578  nsgacs  17802  cycsubg2  17803  gapm  17910  sscntz  17930  pgrpsubgsymgbi  17998  f1omvdcnv  18035  pmtrprfvalrn  18079  odval2  18141  lsmcntz  18263  rhmf1o  18905  isrim  18906  snifpsrbag  19539  gsumply1eq  19848  dfprm2  20015  psgnfix2  20118  islinds3  20346  islindf4  20350  mdetdiaglem  20577  mdetunilem9  20599  slesolinv  20659  slesolex  20661  cpmatel2  20691  m2cpmghm  20722  m2cpminvid2  20733  pm2mpf1  20777  chfacfscmul0  20836  chfacfscmulfsupp  20837  chfacfpmmul0  20840  chfacfpmmulfsupp  20841  isopn2  21009  cmpsub  21376  connsub  21397  ncvs1  23128  rrxmvallem  23358  itg1mulc  23641  lhop1  23947  mdegleb  23994  lawcos  24716  leibpi  24839  2lgslem1a  25286  iscgra  25871  colinearalg  25960  edg0iedg0  26119  edg0iedg0OLD  26120  uhgreq12g  26130  uhgrvtxedgiedgb  26201  usgredg2v  26289  edg0usgr  26315  dfnbgr2  26400  nbuhgr  26409  nbusgredgeu0  26439  nb3grprlem1  26451  nb3grpr  26453  uvtx2vtx1edgb  26475  upgrewlkle2  26683  wlkeq  26710  redwlk  26750  uhgrwkspthlem2  26831  usgr2wlkspth  26836  pthdlem1  26843  cyclnspth  26877  crctcshwlkn0lem1  26884  crctcshwlkn0lem4  26887  crctcsh  26898  iswwlksnx  26914  wlkiswwlksupgr2  26957  wwlksm1edg  26961  wwlksnextsur  26989  wwlksnextproplem3  27000  wwlksnwwlksnonOLD  27006  2wlkdlem4  27019  2wlkdlem5  27020  2pthdlem1  27021  s3wwlks2on  27048  wpthswwlks2on  27053  wpthswwlks2onOLD  27054  elwspths2spth  27060  rusgrnumwwlks  27067  umgrclwwlkge2  27085  clwlkclwwlklem2a4  27091  clwlkclwwlk  27096  clwlkclwwlkflem  27098  clwwisshclwws  27109  isclwwlknx  27135  clwwlknwwlksnb  27156  eclclwwlkn1  27177  clwlksfoclwwlkOLD  27188  clwwlknonel  27213  clwwlknun  27232  clwwlknunOLD  27236  3wlkdlem6  27288  frgrncvvdeqlem9  27432  fusgreg2wsp  27461  numclwwlk2lem1lem  27469  numclwwlk2lem1lemOLD  27470  extwwlkfab  27482  frgrreggt1  27532  ubthlem1  28006  norm-i  28266  hoeq  28899  nmopgt0  29051  pjimai  29315  chirredi  29533  addltmulALT  29585  sbcies  29602  iunrdx  29660  disjrdx  29682  cnvoprabOLD  29778  archiabl  30032  oms0  30639  eulerpartgbij  30714  sgnneg  30882  sgn3da  30883  reprinrn  30976  mrsubrn  31688  sotrine  31936  etasslt  32197  topfne  32626  unbdqndv1  32776  bj-hbntbi  32972  bj-abbi1dv  33058  bj-issetwt  33136  dfgcd3  33452  topdifinfeq  33480  wl-sb6rft  33612  wl-sbalnae  33627  sin2h  33681  poimirlem16  33707  poimirlem17  33708  poimirlem25  33716  mbfresfi  33738  itg2addnclem  33743  itg2addnclem2  33744  itg2addnclem3  33745  ftc1anclem1  33767  isidlc  34096  islshpsm  34739  lshpkrlem1  34869  opcon1b  34957  lautlt  35849  lauteq  35853  idlaut  35854  diblsmopel  36931  doch11  37133  istopclsd  37734  eqrabdioph  37812  rexzrexnn0  37839  zindbi  37982  expdiophlem2  38060  inintabd  38356  cnvcnvintabd  38377  cnvintabd  38380  fsovrfovd  38774  ntrclsiso  38836  ntrneifv3  38851  ntrneineine0lem  38852  ntrneicls11  38859  suprleubrd  38937  suprlubrd  38941  lemuldiv4d  38944  pm14.122a  39094  3impexpbicomi  39157  onfrALTlem5  39228  bitr3VD  39552  onfrALTlem5VD  39589  csbrngVD  39600  pwpwuni  39693  mapsnd  39856  supxrre3  40008  xrralrecnnge  40080  eliooshift  40201  limsupre2lem  40428  liminflimsupclim  40511  xlimbr  40525  smfrec  41471  2reu4a  41664  ralbinrald  41674  afvco2  41731  subsubelfzo0  41815  pfxsuffeqwrdeq  41885  pfxccat3  41905  31prm  41991  dfeven3  42049  iseven5  42055  0noddALTV  42079  2noddALTV  42083  sbgoldbaltlem1  42146  bgoldbtbndlem2  42173  sprvalpwle2  42218  sprsymrelf1lem  42220  0nodd  42289  2nodd  42291  isassintop  42325  rnghmf1o  42382  isrngim  42383  uzlidlring  42408  funcringcsetcALTV2lem8  42522  funcringcsetclem8ALTV  42545  nn0sumltlt  42607  ply1mulgsumlem2  42654  islindeps  42721  lindslinindsimp1  42725  lindslinindsimp2  42731  snlindsntor  42739  zlmodzxznm  42765  ldepslinc  42777  difmodm1lt  42796  elbigo2  42825  elbigolo1  42830  logblt1b  42837  fldivexpfllog2  42838  nnolog2flm1  42863  digexp  42880  nn0sumshdiglemB  42893
  Copyright terms: Public domain W3C validator