Theorem bicomd 140

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 139	. 2 ⊢ ((𝜓 ↔ 𝜒) ↔ (𝜒 ↔ 𝜓))
3	1, 2	sylib 121	1 ⊢ (𝜑 → (𝜒 ↔ 𝜓))

Syntax hints:   → wi 4   ↔ wb 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  impbid2  142  syl5ibr  155  ibir  176  bitr2d  188  bitr3d  189  bitr4d  190  bitr2id  192  bitr2di  196  pm5.5  241  anabs5  563  con2bidc  865  con1biidc  867  con2biidc  869  pm4.63dc  876  pm4.64dc  890  pm5.55dc  903  baibr  910  baibd  913  rbaibd  914  pm4.55dc  928  anordc  946  pm5.75  952  ninba  962  xor3dc  1377  3impexpbicomi  1427  cbvexv1  1740  cbvexh  1743  sbequ12r  1760  sbco  1956  sbcomxyyz  1960  sbal1yz  1989  cbvab  2290  nnedc  2341  necon3bbid  2376  necon2abiidc  2400  necon2bbiidc  2401  sbralie  2710  gencbvex  2772  gencbval  2774  sbhypf  2775  clel3g  2860  reu8  2922  sbceq2a  2961  sbcco2  2973  sbcsng  3635  ssdifsn  3704  opabid  4235  soeq2  4294  tfisi  4564  posng  4676  xpiindim  4741  fvopab6  5582  fconstfvm  5703  cbvfo  5753  cbvexfo  5754  f1eqcocnv  5759  isoid  5778  isoini  5786  resoprab2  5939  dfoprab3  6159  cnvoprab  6202  nnacan  6480  nnmcan  6487  isotilem  6971  eqinfti  6985  inflbti  6989  infglbti  6990  djuf1olem  7018  dfmpq2  7296  axsuploc  7971  div4p1lem1div2  9110  ztri3or  9234  nn0ind-raph  9308  zindd  9309  qreccl  9580  elpq  9586  iooshf  9888  fzofzim  10123  elfzomelpfzo  10166  zmodid2  10287  q2submod  10320  modfzo0difsn  10330  frec2uzltd  10338  frec2uzled  10364  prhash2ex  10722  iserex  11280  prodrbdc  11515  reef11  11640  absdvdsb  11749  dvdsabsb  11750  modmulconst  11763  dvdsadd  11776  dvdsabseq  11785  odd2np1  11810  mod2eq0even  11815  oddnn02np1  11817  oddge22np1  11818  evennn02n  11819  evennn2n  11820  zeo5  11825  gcdass  11948  lcmdvds  12011  lcmass  12017  divgcdcoprm0  12033  divgcdcoprmex  12034  1nprm  12046  dvdsnprmd  12057  isevengcd2  12090  m1dvdsndvds  12180