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  868  pm5.55  957  annotanannot  959  pm5.54  963  baibr  965  rbaib  967  baibd  968  rbaibd  969  ninba  985  pm5.75  998  sbequ12r  2150  cbvalv  2309  sbal1  2488  euor2  2543  abbi1dv  2772  necon3bbid  2860  necon4bbid  2864  ralcom2  3133  gencbvex  3281  sbhypf  3284  alexeqg  3363  clel2g  3370  clel3g  3372  reu8  3435  sbceq2a  3480  sbcco2  3492  reu8nf  3549  raltpd  4346  disjxun  4683  opabid  5011  soeq2  5084  posn  5221  xpiindi  5290  fvopab6  6350  cbvfo  6584  f1eqcocnv  6596  isoid  6619  isoini  6628  isosolem  6637  riotaeqimp  6674  resoprab2  6799  tfisi  7100  tfinds2  7105  f1oweALT  7194  dfoprab3  7268  opiota  7273  mpt2curryd  7440  oalimcl  7685  omword  7695  oeword  7715  nnacan  7753  nnmcan  7759  findcard2s  8242  funisfsupp  8321  suppeqfsuppbi  8330  eqinf  8431  inflb  8436  infglb  8437  infglbb  8438  infltoreq  8449  infempty  8453  brwdomn0  8515  cantnfp1lem3  8615  ssrankr1  8736  r1pw  8746  aleph11  8945  alephval3  8971  gch-kn  9537  wunex2  9598  lttri2  10158  wloglei  10598  divne0b  10734  lemul1  10913  nnnle0  11089  div4p1lem1div2  11325  nn0ind-raph  11515  zindd  11516  suprfinzcl  11530  rebtwnz  11825  qreccl  11846  xrlttri2  12013  2resupmax  12057  xmulneg1  12137  iooshf  12290  difreicc  12342  fzofzim  12554  elfzomelpfzo  12612  elfznelfzo  12613  divfl0  12665  zmodid2  12738  2submod  12771  modfzo0difsn  12782  om2uzlti  12789  expcan  12953  hashvnfin  13189  hashneq0  13193  prhash2ex  13225  hashgt0elex  13227  hashgt12el  13248  hashgt12el2  13249  hashbclem  13274  hashf1lem2  13278  prprrab  13293  swrdn0  13476  swrd0  13480  2swrdeqwrdeq  13499  swrdswrd  13506  swrdccat3  13538  repswswrd  13577  cshf1  13602  cshw1repsw  13615  relexpindlem  13847  absz  14095  iserex  14431  prodrb  14706  absdvdsb  15047  dvdsabsb  15048  modmulconst  15060  dvdsadd  15071  dvdsabseq  15082  mod2eq0even  15117  oddnn02np1  15119  oddge22np1  15120  evennn02n  15121  evennn2n  15122  zeo5  15127  sadadd2lem2  15219  smupvallem  15252  gcdass  15311  lcmdvds  15368  lcmass  15374  divgcdcoprm0  15426  divgcdcoprmex  15427  1nprm  15439  dvdsnprmd  15450  ncoprmlnprm  15483  isevengcd2  15485  m1dvdsndvds  15550  cshws0  15855  sbcie2s  15963  sbcie3s  15964  dfiso2  16479  initoid  16702  termoid  16703  funcestrcsetclem8  16834  lublecllem  17035  odudlatb  17243  issubm2  17395  mgm2nsgrplem2  17453  nsgacs  17677  cycsubg2  17678  gapm  17785  sscntz  17805  pgrpsubgsymgbi  17873  f1omvdcnv  17910  pmtrprfvalrn  17954  odval2  18016  lsmcntz  18138  rhmf1o  18780  isrim  18781  snifpsrbag  19414  gsumply1eq  19723  dfprm2  19890  psgnfix2  19993  islinds3  20221  islindf4  20225  mdetdiaglem  20452  mdetunilem9  20474  slesolinv  20534  slesolex  20536  cpmatel2  20566  m2cpmghm  20597  m2cpminvid2  20608  pm2mpf1  20652  chfacfscmul0  20711  chfacfscmulfsupp  20712  chfacfpmmul0  20715  chfacfpmmulfsupp  20716  isopn2  20884  cmpsub  21251  connsub  21272  ncvs1  23003  rrxmvallem  23233  itg1mulc  23516  lhop1  23822  mdegleb  23869  lawcos  24591  leibpi  24714  2lgslem1a  25161  iscgra  25746  colinearalg  25835  edg0iedg0  25994  edg0iedg0OLD  25995  uhgreq12g  26005  uhgrvtxedgiedgb  26076  usgredg2v  26164  edg0usgr  26190  dfnbgr2  26275  nbuhgr  26284  nbusgredgeu0  26314  nb3grprlem1  26326  nb3grpr  26328  uvtx2vtx1edgb  26350  upgrewlkle2  26558  wlkeq  26585  redwlk  26625  uhgrwkspthlem2  26706  usgr2wlkspth  26711  pthdlem1  26718  cyclnspth  26751  crctcshwlkn0lem1  26758  crctcshwlkn0lem4  26761  crctcsh  26772  iswwlksnx  26788  wlkiswwlksupgr2  26831  wwlksm1edg  26835  wwlksnextsur  26863  wwlksnextproplem3  26874  wwlksnwwlksnonOLD  26880  2wlkdlem4  26893  2wlkdlem5  26894  2pthdlem1  26895  s3wwlks2on  26922  wpthswwlks2on  26927  wpthswwlks2onOLD  26928  elwspths2spth  26934  rusgrnumwwlks  26941  umgrclwwlkge2  26957  clwlkclwwlklem2a4  26963  clwlkclwwlk  26968  clwwisshclwws  26972  isclwwlknx  26998  clwwlknwwlksnb  27019  eclclwwlkn1  27039  clwlksfoclwwlk  27050  clwwlknonel  27070  clwwlknun  27087  clwwlknunOLD  27091  3wlkdlem6  27143  frgrncvvdeqlem9  27287  fusgreg2wsp  27316  numclwwlk2lem1lem  27324  numclwwlk2lem1lemOLD  27325  extwwlkfab  27342  frgrreggt1  27380  ubthlem1  27854  norm-i  28114  hoeq  28747  nmopgt0  28899  pjimai  29163  chirredi  29381  addltmulALT  29433  sbcies  29450  iunrdx  29508  disjrdx  29530  cnvoprabOLD  29626  archiabl  29880  oms0  30487  eulerpartgbij  30562  sgnneg  30730  sgn3da  30731  reprinrn  30824  mrsubrn  31536  sotrine  31784  etasslt  32045  topfne  32474  unbdqndv1  32624  bj-hbntbi  32820  bj-abbi1dv  32906  bj-issetwt  32984  dfgcd3  33300  topdifinfeq  33328  wl-sb6rft  33460  wl-sbalnae  33475  sin2h  33529  poimirlem16  33555  poimirlem17  33556  poimirlem25  33564  mbfresfi  33586  itg2addnclem  33591  itg2addnclem2  33592  itg2addnclem3  33593  ftc1anclem1  33615  isidlc  33944  islshpsm  34585  lshpkrlem1  34715  opcon1b  34803  lautlt  35695  lauteq  35699  idlaut  35700  diblsmopel  36777  doch11  36979  istopclsd  37580  eqrabdioph  37658  rexzrexnn0  37685  zindbi  37828  expdiophlem2  37906  inintabd  38202  cnvcnvintabd  38223  cnvintabd  38226  fsovrfovd  38620  ntrclsiso  38682  ntrneifv3  38697  ntrneineine0lem  38698  ntrneicls11  38705  suprleubrd  38783  suprlubrd  38787  lemuldiv4d  38790  pm14.122a  38940  3impexpbicomi  39003  onfrALTlem5  39074  bitr3VD  39398  onfrALTlem5VD  39435  csbrngVD  39446  pwpwuni  39539  mapsnd  39702  supxrre3  39854  xrralrecnnge  39926  eliooshift  40047  limsupre2lem  40274  liminflimsupclim  40357  xlimbr  40371  smfrec  41317  2reu4a  41510  ralbinrald  41520  afvco2  41577  subsubelfzo0  41661  pfxsuffeqwrdeq  41731  pfxccat3  41751  31prm  41837  dfeven3  41895  iseven5  41901  0noddALTV  41925  2noddALTV  41929  sbgoldbaltlem1  41992  bgoldbtbndlem2  42019  sprvalpwle2  42064  sprsymrelf1lem  42066  0nodd  42135  2nodd  42137  isassintop  42171  rnghmf1o  42228  isrngim  42229  uzlidlring  42254  funcringcsetcALTV2lem8  42368  funcringcsetclem8ALTV  42391  nn0sumltlt  42453  ply1mulgsumlem2  42500  islindeps  42567  lindslinindsimp1  42571  lindslinindsimp2  42577  snlindsntor  42585  zlmodzxznm  42611  ldepslinc  42623  difmodm1lt  42642  elbigo2  42671  elbigolo1  42676  logblt1b  42683  fldivexpfllog2  42684  nnolog2flm1  42709  digexp  42726  nn0sumshdiglemB  42739
  Copyright terms: Public domain W3C validator