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  annotanannot  676  con2bidc  883  con1biidc  885  con2biidc  887  pm4.63dc  894  pm4.64dc  908  pm5.55dc  921  baibr  928  baibd  931  rbaibd  932  pm5.75  971  ninba  981  xor3dc  1432  3impexpbicomi  1485  cbvexv1  1800  cbvexh  1803  sbequ12r  1820  sbco  2021  sbcomxyyz  2025  sbal1yz  2054  cbvab  2356  nnedc  2408  necon3bbid  2443  necon2abiidc  2467  necon2bbiidc  2468  sbralie  2786  gencbvex  2851  gencbval  2853  sbhypf  2854  clel3g  2941  reu8  3003  sbceq2a  3043  sbcco2  3055  reu8nf  3114  sbcsng  3732  ssdifsn  3805  opabid  4356  soeq2  4419  tfisi  4691  posng  4804  xpiindim  4873  fvopab6  5752  fconstfvm  5880  cbvfo  5936  cbvexfo  5937  f1eqcocnv  5942  isoid  5961  isoini  5969  riotaeqimp  6006  resoprab2  6128  dfoprab3  6363  cnvoprab  6408  nnacan  6723  nnmcan  6730  isotilem  7248  eqinfti  7262  inflbti  7266  infglbti  7267  djuf1olem  7295  dfmpq2  7618  axsuploc  8294  div4p1lem1div2  9440  ztri3or  9566  nn0ind-raph  9641  zindd  9642  qreccl  9920  elpq  9927  iooshf  10231  fzofzim  10473  elfzomelpfzo  10522  zmodid2  10660  q2submod  10693  modfzo0difsn  10703  frec2uzltd  10711  frec2uzled  10737  prhash2ex  11119  swrd0g  11290  pfxn0  11318  swrdswrd  11335  pfxccat3  11364  iserex  11962  prodrbdc  12198  reef11  12323  absdvdsb  12433  dvdsabsb  12434  modmulconst  12447  dvdsadd  12460  dvdsabseq  12471  odd2np1  12497  mod2eq0even  12502  oddnn02np1  12504  oddge22np1  12505  evennn02n  12506  evennn2n  12507  zeo5  12512  gcdass  12649  lcmdvds  12714  lcmass  12720  divgcdcoprm0  12736  divgcdcoprmex  12737  1nprm  12749  dvdsnprmd  12760  isevengcd2  12793  m1dvdsndvds  12884  sgrppropd  13559  issubm2  13619  rngpropd  14032  rhmf1o  14246  isrim  14247  2lgslem1a  15890  edg0iedg0g  15990  uhgreq12g  16000  uhgrvtxedgiedgb  16067  edg0usgr  16171  umgrclwwlkge2  16326  isclwwlknx  16340  clwwlknonel  16356  clwwlknun  16365