Theorem bicomd 141

Description: Commute two sides of a biconditional in a deduction. (Contributed by NM, 5-Aug-1993.)

Hypothesis

Ref	Expression
bicomd.1	⊢ (𝜑 → (𝜓 ↔ 𝜒))

Assertion

Ref	Expression
bicomd	⊢ (𝜑 → (𝜒 ↔ 𝜓))

Proof of Theorem bicomd

Step	Hyp	Ref	Expression
1		bicomd.1	. 2 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
2		bicom 140	. 2 ⊢ ((𝜓 ↔ 𝜒) ↔ (𝜒 ↔ 𝜓))
3	1, 2	sylib 122	1 ⊢ (𝜑 → (𝜒 ↔ 𝜓))

Syntax hints:   → wi 4   ↔ wb 105

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  impbid2  143  imbitrrid  156  ibir  177  bitr2d  189  bitr3d  190  bitr4d  191  bitr2id  193  bitr2di  197  pm5.5  242  anabs5  573  con2bidc  876  con1biidc  878  con2biidc  880  pm4.63dc  887  pm4.64dc  901  pm5.55dc  914  baibr  921  baibd  924  rbaibd  925  pm5.75  964  ninba  974  xor3dc  1398  3impexpbicomi  1450  cbvexv1  1763  cbvexh  1766  sbequ12r  1783  sbco  1984  sbcomxyyz  1988  sbal1yz  2017  cbvab  2317  nnedc  2369  necon3bbid  2404  necon2abiidc  2428  necon2bbiidc  2429  sbralie  2744  gencbvex  2807  gencbval  2809  sbhypf  2810  clel3g  2895  reu8  2957  sbceq2a  2997  sbcco2  3009  sbcsng  3678  ssdifsn  3747  opabid  4287  soeq2  4348  tfisi  4620  posng  4732  xpiindim  4800  fvopab6  5655  fconstfvm  5777  cbvfo  5829  cbvexfo  5830  f1eqcocnv  5835  isoid  5854  isoini  5862  resoprab2  6016  dfoprab3  6246  cnvoprab  6289  nnacan  6567  nnmcan  6574  isotilem  7067  eqinfti  7081  inflbti  7085  infglbti  7086  djuf1olem  7114  dfmpq2  7417  axsuploc  8094  div4p1lem1div2  9239  ztri3or  9363  nn0ind-raph  9437  zindd  9438  qreccl  9710  elpq  9717  iooshf  10021  fzofzim  10258  elfzomelpfzo  10301  zmodid2  10426  q2submod  10459  modfzo0difsn  10469  frec2uzltd  10477  frec2uzled  10503  prhash2ex  10883  iserex  11485  prodrbdc  11720  reef11  11845  absdvdsb  11955  dvdsabsb  11956  modmulconst  11969  dvdsadd  11982  dvdsabseq  11992  odd2np1  12017  mod2eq0even  12022  oddnn02np1  12024  oddge22np1  12025  evennn02n  12026  evennn2n  12027  zeo5  12032  gcdass  12155  lcmdvds  12220  lcmass  12226  divgcdcoprm0  12242  divgcdcoprmex  12243  1nprm  12255  dvdsnprmd  12266  isevengcd2  12299  m1dvdsndvds  12389  sgrppropd  12999  issubm2  13048  rngpropd  13454  rhmf1o  13667  isrim  13668  2lgslem1a  15245