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  579  annotanannot  680  con2bidc  887  con1biidc  889  con2biidc  891  pm4.63dc  898  pm4.64dc  912  pm5.55dc  925  baibr  932  baibd  935  rbaibd  936  pm5.75  975  ninba  985  xor3dc  1436  3impexpbicomi  1489  cbvexv1  1805  cbvexh  1808  sbequ12r  1825  sbco  2028  sbcomxyyz  2032  sbal1yz  2061  cbvab  2364  eqabcdv  2370  nnedc  2425  necon3bbid  2460  necon2abiidc  2484  necon2bbiidc  2485  sbralie  2804  gencbvex  2869  gencbval  2871  sbhypf  2872  clel3g  2960  reu8  3022  sbceq2a  3062  sbcco2  3074  reu8nf  3133  sbcsng  3764  ssdifsn  3837  opabid  4393  soeq2  4456  tfisi  4729  posng  4842  xpiindim  4912  fvopab6  5796  fconstfvm  5924  cbvfo  5981  cbvexfo  5982  f1eqcocnv  5987  isoid  6006  isoini  6014  riotaeqimp  6053  resoprab2  6175  dfoprab3  6415  cnvoprab  6460  nnacan  6775  nnmcan  6782  mapsnd  6960  funisfsupp  7281  suppeqfsuppbi  7285  isotilem  7336  eqinfti  7350  inflbti  7354  infglbti  7355  djuf1olem  7383  dfmpq2  7712  axsuploc  8388  div4p1lem1div2  9538  ztri3or  9666  nn0ind-raph  9742  zindd  9743  qreccl  10021  elpq  10028  iooshf  10333  fzofzim  10578  elfzomelpfzo  10627  zmodid2  10767  q2submod  10800  modfzo0difsn  10810  frec2uzltd  10818  frec2uzled  10844  prhash2ex  11228  hashf1lem2  11264  swrd0g  11410  pfxn0  11438  swrdswrd  11455  pfxccat3  11484  iserex  12083  prodrbdc  12319  reef11  12444  absdvdsb  12554  dvdsabsb  12555  modmulconst  12568  dvdsadd  12581  dvdsabseq  12592  odd2np1  12618  mod2eq0even  12623  oddnn02np1  12625  oddge22np1  12626  evennn02n  12627  evennn2n  12628  zeo5  12633  gcdass  12770  lcmdvds  12835  lcmass  12841  divgcdcoprm0  12857  divgcdcoprmex  12858  1nprm  12870  dvdsnprmd  12881  isevengcd2  12914  m1dvdsndvds  13005  sgrppropd  13705  issubm2  13757  rngpropd  14229  rhmf1o  14448  isrim  14449  2lgslem1a  16121  edg0iedg0g  16221  uhgreq12g  16231  uhgrvtxedgiedgb  16298  edg0usgr  16402  umgrclwwlkge2  16557  isclwwlknx  16571  clwwlknonel  16587  clwwlknun  16596