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  575  con2bidc  882  con1biidc  884  con2biidc  886  pm4.63dc  893  pm4.64dc  907  pm5.55dc  920  baibr  927  baibd  930  rbaibd  931  pm5.75  970  ninba  980  xor3dc  1431  3impexpbicomi  1484  cbvexv1  1800  cbvexh  1803  sbequ12r  1820  sbco  2021  sbcomxyyz  2025  sbal1yz  2054  cbvab  2355  nnedc  2407  necon3bbid  2442  necon2abiidc  2466  necon2bbiidc  2467  sbralie  2785  gencbvex  2850  gencbval  2852  sbhypf  2853  clel3g  2940  reu8  3002  sbceq2a  3042  sbcco2  3054  reu8nf  3113  sbcsng  3728  ssdifsn  3801  opabid  4350  soeq2  4413  tfisi  4685  posng  4798  xpiindim  4867  fvopab6  5743  fconstfvm  5871  cbvfo  5925  cbvexfo  5926  f1eqcocnv  5931  isoid  5950  isoini  5958  riotaeqimp  5995  resoprab2  6117  dfoprab3  6353  cnvoprab  6398  nnacan  6679  nnmcan  6686  isotilem  7204  eqinfti  7218  inflbti  7222  infglbti  7223  djuf1olem  7251  dfmpq2  7574  axsuploc  8251  div4p1lem1div2  9397  ztri3or  9521  nn0ind-raph  9596  zindd  9597  qreccl  9875  elpq  9882  iooshf  10186  fzofzim  10426  elfzomelpfzo  10475  zmodid2  10613  q2submod  10646  modfzo0difsn  10656  frec2uzltd  10664  frec2uzled  10690  prhash2ex  11072  swrd0g  11240  pfxn0  11268  swrdswrd  11285  pfxccat3  11314  iserex  11899  prodrbdc  12134  reef11  12259  absdvdsb  12369  dvdsabsb  12370  modmulconst  12383  dvdsadd  12396  dvdsabseq  12407  odd2np1  12433  mod2eq0even  12438  oddnn02np1  12440  oddge22np1  12441  evennn02n  12442  evennn2n  12443  zeo5  12448  gcdass  12585  lcmdvds  12650  lcmass  12656  divgcdcoprm0  12672  divgcdcoprmex  12673  1nprm  12685  dvdsnprmd  12696  isevengcd2  12729  m1dvdsndvds  12820  sgrppropd  13495  issubm2  13555  rngpropd  13967  rhmf1o  14181  isrim  14182  2lgslem1a  15816  edg0iedg0g  15916  uhgreq12g  15926  uhgrvtxedgiedgb  15993  edg0usgr  16097  umgrclwwlkge2  16252  isclwwlknx  16266  clwwlknonel  16282  clwwlknun  16291