Theorem bicomd 139

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

Syntax hints:   → wi 4   ↔ wb 103

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

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  impbid2  141  syl5ibr  154  ibir  175  bitr2d  187  bitr3d  188  bitr4d  189  syl5rbb  191  syl6rbb  195  pm5.5  240  anabs5  537  con2bidc  802  con1biidc  804  con2biidc  806  pm4.63dc  813  pm4.64dc  834  pm5.55dc  852  baibr  862  baibd  865  rbaibd  866  pm4.55dc  879  anordc  897  pm5.75  903  ninba  913  xor3dc  1318  3impexpbicomi  1368  cbvexh  1678  sbequ12r  1695  sbco  1883  sbcomxyyz  1887  sbal1yz  1918  cbvab  2201  nnedc  2250  necon3bbid  2285  necon2abiidc  2309  necon2bbii  2310  gencbvex  2645  gencbval  2647  sbhypf  2648  clel3g  2729  reu8  2788  sbceq2a  2825  sbcco2  2837  sbcsng  3451  opabid  4012  soeq2  4071  tfisi  4328  posng  4430  xpiindim  4491  fvopab6  5285  fconstfvm  5400  cbvfo  5445  cbvexfo  5446  f1eqcocnv  5451  isoid  5470  isoini  5477  resoprab2  5618  dfoprab3  5837  cnvoprab  5875  nnacan  6108  nnmcan  6115  isotilem  6419  eqinfti  6433  inflbti  6437  infglbti  6438  dfmpq2  6545  div4p1lem1div2  8284  ztri3or  8394  nn0ind-raph  8464  zindd  8465  qreccl  8727  iooshf  8975  fzofzim  9197  elfzomelpfzo  9240  zmodid2  9354  q2submod  9387  modfzo0difsn  9397  frec2uzltd  9405  iiserex  10177  absdvdsb  10213  dvdsabsb  10214  modmulconst  10227  dvdsadd  10238  dvdsabseq  10247  odd2np1  10272  mod2eq0even  10277  oddnn02np1  10280  oddge22np1  10281  evennn02n  10282  evennn2n  10283  zeo5  10288  gcdass  10404  lcmdvds  10461  lcmass  10467  divgcdcoprm0  10483  divgcdcoprmex  10484  1nprm  10496  dvdsnprmd  10507  isevengcd2  10537  bj-indeq  10724