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  1766  cbvexh  1769  sbequ12r  1786  sbco  1987  sbcomxyyz  1991  sbal1yz  2020  cbvab  2320  nnedc  2372  necon3bbid  2407  necon2abiidc  2431  necon2bbiidc  2432  sbralie  2747  gencbvex  2810  gencbval  2812  sbhypf  2813  clel3g  2898  reu8  2960  sbceq2a  3000  sbcco2  3012  sbcsng  3682  ssdifsn  3751  opabid  4291  soeq2  4352  tfisi  4624  posng  4736  xpiindim  4804  fvopab6  5661  fconstfvm  5783  cbvfo  5835  cbvexfo  5836  f1eqcocnv  5841  isoid  5860  isoini  5868  resoprab2  6023  dfoprab3  6258  cnvoprab  6301  nnacan  6579  nnmcan  6586  isotilem  7081  eqinfti  7095  inflbti  7099  infglbti  7100  djuf1olem  7128  dfmpq2  7439  axsuploc  8116  div4p1lem1div2  9262  ztri3or  9386  nn0ind-raph  9460  zindd  9461  qreccl  9733  elpq  9740  iooshf  10044  fzofzim  10281  elfzomelpfzo  10324  zmodid2  10461  q2submod  10494  modfzo0difsn  10504  frec2uzltd  10512  frec2uzled  10538  prhash2ex  10918  iserex  11521  prodrbdc  11756  reef11  11881  absdvdsb  11991  dvdsabsb  11992  modmulconst  12005  dvdsadd  12018  dvdsabseq  12029  odd2np1  12055  mod2eq0even  12060  oddnn02np1  12062  oddge22np1  12063  evennn02n  12064  evennn2n  12065  zeo5  12070  gcdass  12207  lcmdvds  12272  lcmass  12278  divgcdcoprm0  12294  divgcdcoprmex  12295  1nprm  12307  dvdsnprmd  12318  isevengcd2  12351  m1dvdsndvds  12442  sgrppropd  13115  issubm2  13175  rngpropd  13587  rhmf1o  13800  isrim  13801  2lgslem1a  15413