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  1763  cbvexh  1766  sbequ12r  1783  sbco  1984  sbcomxyyz  1988  sbal1yz  2017  cbvab  2317  nnedc  2369  necon3bbid  2404  necon2abiidc  2428  necon2bbiidc  2429  sbralie  2744  gencbvex  2806  gencbval  2808  sbhypf  2809  clel3g  2894  reu8  2956  sbceq2a  2996  sbcco2  3008  sbcsng  3677  ssdifsn  3746  opabid  4286  soeq2  4347  tfisi  4619  posng  4731  xpiindim  4799  fvopab6  5654  fconstfvm  5776  cbvfo  5828  cbvexfo  5829  f1eqcocnv  5834  isoid  5853  isoini  5861  resoprab2  6015  dfoprab3  6244  cnvoprab  6287  nnacan  6565  nnmcan  6572  isotilem  7065  eqinfti  7079  inflbti  7083  infglbti  7084  djuf1olem  7112  dfmpq2  7415  axsuploc  8092  div4p1lem1div2  9236  ztri3or  9360  nn0ind-raph  9434  zindd  9435  qreccl  9707  elpq  9714  iooshf  10018  fzofzim  10255  elfzomelpfzo  10298  zmodid2  10423  q2submod  10456  modfzo0difsn  10466  frec2uzltd  10474  frec2uzled  10500  prhash2ex  10880  iserex  11482  prodrbdc  11717  reef11  11842  absdvdsb  11952  dvdsabsb  11953  modmulconst  11966  dvdsadd  11979  dvdsabseq  11989  odd2np1  12014  mod2eq0even  12019  oddnn02np1  12021  oddge22np1  12022  evennn02n  12023  evennn2n  12024  zeo5  12029  gcdass  12152  lcmdvds  12217  lcmass  12223  divgcdcoprm0  12239  divgcdcoprmex  12240  1nprm  12252  dvdsnprmd  12263  isevengcd2  12296  m1dvdsndvds  12386  sgrppropd  12996  issubm2  13045  rngpropd  13451  rhmf1o  13664  isrim  13665