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  7441  axsuploc  8118  div4p1lem1div2  9264  ztri3or  9388  nn0ind-raph  9462  zindd  9463  qreccl  9735  elpq  9742  iooshf  10046  fzofzim  10283  elfzomelpfzo  10326  zmodid2  10463  q2submod  10496  modfzo0difsn  10506  frec2uzltd  10514  frec2uzled  10540  prhash2ex  10920  iserex  11523  prodrbdc  11758  reef11  11883  absdvdsb  11993  dvdsabsb  11994  modmulconst  12007  dvdsadd  12020  dvdsabseq  12031  odd2np1  12057  mod2eq0even  12062  oddnn02np1  12064  oddge22np1  12065  evennn02n  12066  evennn2n  12067  zeo5  12072  gcdass  12209  lcmdvds  12274  lcmass  12280  divgcdcoprm0  12296  divgcdcoprmex  12297  1nprm  12309  dvdsnprmd  12320  isevengcd2  12353  m1dvdsndvds  12444  sgrppropd  13117  issubm2  13177  rngpropd  13589  rhmf1o  13802  isrim  13803  2lgslem1a  15437