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  880  con1biidc  882  con2biidc  884  pm4.63dc  891  pm4.64dc  905  pm5.55dc  918  baibr  925  baibd  928  rbaibd  929  pm5.75  968  ninba  978  xor3dc  1429  3impexpbicomi  1482  cbvexv1  1798  cbvexh  1801  sbequ12r  1818  sbco  2019  sbcomxyyz  2023  sbal1yz  2052  cbvab  2353  nnedc  2405  necon3bbid  2440  necon2abiidc  2464  necon2bbiidc  2465  sbralie  2783  gencbvex  2847  gencbval  2849  sbhypf  2850  clel3g  2937  reu8  2999  sbceq2a  3039  sbcco2  3051  reu8nf  3110  sbcsng  3725  ssdifsn  3796  opabid  4344  soeq2  4407  tfisi  4679  posng  4791  xpiindim  4859  fvopab6  5733  fconstfvm  5861  cbvfo  5915  cbvexfo  5916  f1eqcocnv  5921  isoid  5940  isoini  5948  riotaeqimp  5985  resoprab2  6107  dfoprab3  6343  cnvoprab  6386  nnacan  6666  nnmcan  6673  isotilem  7184  eqinfti  7198  inflbti  7202  infglbti  7203  djuf1olem  7231  dfmpq2  7553  axsuploc  8230  div4p1lem1div2  9376  ztri3or  9500  nn0ind-raph  9575  zindd  9576  qreccl  9849  elpq  9856  iooshf  10160  fzofzim  10400  elfzomelpfzo  10449  zmodid2  10586  q2submod  10619  modfzo0difsn  10629  frec2uzltd  10637  frec2uzled  10663  prhash2ex  11044  swrd0g  11207  pfxn0  11235  swrdswrd  11252  pfxccat3  11281  iserex  11865  prodrbdc  12100  reef11  12225  absdvdsb  12335  dvdsabsb  12336  modmulconst  12349  dvdsadd  12362  dvdsabseq  12373  odd2np1  12399  mod2eq0even  12404  oddnn02np1  12406  oddge22np1  12407  evennn02n  12408  evennn2n  12409  zeo5  12414  gcdass  12551  lcmdvds  12616  lcmass  12622  divgcdcoprm0  12638  divgcdcoprmex  12639  1nprm  12651  dvdsnprmd  12662  isevengcd2  12695  m1dvdsndvds  12786  sgrppropd  13461  issubm2  13521  rngpropd  13933  rhmf1o  14147  isrim  14148  2lgslem1a  15782  edg0iedg0g  15881  uhgreq12g  15891  uhgrvtxedgiedgb  15956  umgrclwwlkge2  16139