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  1406  3impexpbicomi  1458  cbvexv1  1774  cbvexh  1777  sbequ12r  1794  sbco  1995  sbcomxyyz  1999  sbal1yz  2028  cbvab  2328  nnedc  2380  necon3bbid  2415  necon2abiidc  2439  necon2bbiidc  2440  sbralie  2755  gencbvex  2818  gencbval  2820  sbhypf  2821  clel3g  2906  reu8  2968  sbceq2a  3008  sbcco2  3020  sbcsng  3691  ssdifsn  3760  opabid  4301  soeq2  4362  tfisi  4634  posng  4746  xpiindim  4814  fvopab6  5675  fconstfvm  5801  cbvfo  5853  cbvexfo  5854  f1eqcocnv  5859  isoid  5878  isoini  5886  resoprab2  6041  dfoprab3  6276  cnvoprab  6319  nnacan  6597  nnmcan  6604  isotilem  7107  eqinfti  7121  inflbti  7125  infglbti  7126  djuf1olem  7154  dfmpq2  7467  axsuploc  8144  div4p1lem1div2  9290  ztri3or  9414  nn0ind-raph  9489  zindd  9490  qreccl  9762  elpq  9769  iooshf  10073  fzofzim  10310  elfzomelpfzo  10358  zmodid2  10495  q2submod  10528  modfzo0difsn  10538  frec2uzltd  10546  frec2uzled  10572  prhash2ex  10952  iserex  11621  prodrbdc  11856  reef11  11981  absdvdsb  12091  dvdsabsb  12092  modmulconst  12105  dvdsadd  12118  dvdsabseq  12129  odd2np1  12155  mod2eq0even  12160  oddnn02np1  12162  oddge22np1  12163  evennn02n  12164  evennn2n  12165  zeo5  12170  gcdass  12307  lcmdvds  12372  lcmass  12378  divgcdcoprm0  12394  divgcdcoprmex  12395  1nprm  12407  dvdsnprmd  12418  isevengcd2  12451  m1dvdsndvds  12542  sgrppropd  13216  issubm2  13276  rngpropd  13688  rhmf1o  13901  isrim  13902  2lgslem1a  15536