Theorem bicomd 140

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 139	. 2 ⊢ ((𝜓 ↔ 𝜒) ↔ (𝜒 ↔ 𝜓))
3	1, 2	sylib 121	1 ⊢ (𝜑 → (𝜒 ↔ 𝜓))

Syntax hints:   → wi 4   ↔ wb 104

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

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  impbid2  142  syl5ibr  155  ibir  176  bitr2d  188  bitr3d  189  bitr4d  190  syl5rbb  192  syl6rbb  196  pm5.5  241  anabs5  543  con2bidc  813  con1biidc  815  con2biidc  817  pm4.63dc  824  pm4.64dc  845  pm5.55dc  863  baibr  873  baibd  876  rbaibd  877  pm4.55dc  890  anordc  908  pm5.75  914  ninba  924  xor3dc  1333  3impexpbicomi  1383  cbvexh  1696  sbequ12r  1713  sbco  1902  sbcomxyyz  1906  sbal1yz  1937  cbvab  2222  nnedc  2272  necon3bbid  2307  necon2abiidc  2331  necon2bbiidc  2332  gencbvex  2687  gencbval  2689  sbhypf  2690  clel3g  2773  reu8  2833  sbceq2a  2872  sbcco2  2884  sbcsng  3529  ssdifsn  3598  opabid  4117  soeq2  4176  tfisi  4439  posng  4549  xpiindim  4614  fvopab6  5449  fconstfvm  5570  cbvfo  5618  cbvexfo  5619  f1eqcocnv  5624  isoid  5643  isoini  5651  resoprab2  5800  dfoprab3  6019  cnvoprab  6061  nnacan  6338  nnmcan  6345  isotilem  6808  eqinfti  6822  inflbti  6826  infglbti  6827  djuf1olem  6853  dfmpq2  7064  div4p1lem1div2  8825  ztri3or  8949  nn0ind-raph  9020  zindd  9021  qreccl  9284  iooshf  9576  fzofzim  9806  elfzomelpfzo  9849  zmodid2  9966  q2submod  9999  modfzo0difsn  10009  frec2uzltd  10017  frec2uzled  10043  prhash2ex  10396  iserex  10947  reef11  11204  absdvdsb  11306  dvdsabsb  11307  modmulconst  11320  dvdsadd  11331  dvdsabseq  11340  odd2np1  11365  mod2eq0even  11370  oddnn02np1  11372  oddge22np1  11373  evennn02n  11374  evennn2n  11375  zeo5  11380  gcdass  11496  lcmdvds  11553  lcmass  11559  divgcdcoprm0  11575  divgcdcoprmex  11576  1nprm  11588  dvdsnprmd  11599  isevengcd2  11629  bj-indeq  12712