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  877  con1biidc  879  con2biidc  881  pm4.63dc  888  pm4.64dc  902  pm5.55dc  915  baibr  922  baibd  925  rbaibd  926  pm5.75  965  ninba  975  xor3dc  1407  3impexpbicomi  1460  cbvexv1  1776  cbvexh  1779  sbequ12r  1796  sbco  1997  sbcomxyyz  2001  sbal1yz  2030  cbvab  2331  nnedc  2383  necon3bbid  2418  necon2abiidc  2442  necon2bbiidc  2443  sbralie  2760  gencbvex  2824  gencbval  2826  sbhypf  2827  clel3g  2914  reu8  2976  sbceq2a  3016  sbcco2  3028  reu8nf  3087  sbcsng  3702  ssdifsn  3772  opabid  4320  soeq2  4381  tfisi  4653  posng  4765  xpiindim  4833  fvopab6  5699  fconstfvm  5825  cbvfo  5877  cbvexfo  5878  f1eqcocnv  5883  isoid  5902  isoini  5910  resoprab2  6065  dfoprab3  6300  cnvoprab  6343  nnacan  6621  nnmcan  6628  isotilem  7134  eqinfti  7148  inflbti  7152  infglbti  7153  djuf1olem  7181  dfmpq2  7503  axsuploc  8180  div4p1lem1div2  9326  ztri3or  9450  nn0ind-raph  9525  zindd  9526  qreccl  9798  elpq  9805  iooshf  10109  fzofzim  10349  elfzomelpfzo  10397  zmodid2  10534  q2submod  10567  modfzo0difsn  10577  frec2uzltd  10585  frec2uzled  10611  prhash2ex  10991  swrd0g  11151  pfxn0  11179  swrdswrd  11196  pfxccat3  11225  iserex  11765  prodrbdc  12000  reef11  12125  absdvdsb  12235  dvdsabsb  12236  modmulconst  12249  dvdsadd  12262  dvdsabseq  12273  odd2np1  12299  mod2eq0even  12304  oddnn02np1  12306  oddge22np1  12307  evennn02n  12308  evennn2n  12309  zeo5  12314  gcdass  12451  lcmdvds  12516  lcmass  12522  divgcdcoprm0  12538  divgcdcoprmex  12539  1nprm  12551  dvdsnprmd  12562  isevengcd2  12595  m1dvdsndvds  12686  sgrppropd  13360  issubm2  13420  rngpropd  13832  rhmf1o  14045  isrim  14046  2lgslem1a  15680  edg0iedg0g  15777  uhgreq12g  15787  uhgrvtxedgiedgb  15847