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  syl5ibr  156  ibir  177  bitr2d  189  bitr3d  190  bitr4d  191  bitr2id  193  bitr2di  197  pm5.5  242  anabs5  573  con2bidc  875  con1biidc  877  con2biidc  879  pm4.63dc  886  pm4.64dc  900  pm5.55dc  913  baibr  920  baibd  923  rbaibd  924  pm4.55dc  938  anordc  956  pm5.75  962  ninba  972  xor3dc  1387  3impexpbicomi  1437  cbvexv1  1750  cbvexh  1753  sbequ12r  1770  sbco  1966  sbcomxyyz  1970  sbal1yz  1999  cbvab  2299  nnedc  2350  necon3bbid  2385  necon2abiidc  2409  necon2bbiidc  2410  sbralie  2719  gencbvex  2781  gencbval  2783  sbhypf  2784  clel3g  2869  reu8  2931  sbceq2a  2971  sbcco2  2983  sbcsng  3648  ssdifsn  3717  opabid  4251  soeq2  4310  tfisi  4580  posng  4692  xpiindim  4757  fvopab6  5604  fconstfvm  5726  cbvfo  5776  cbvexfo  5777  f1eqcocnv  5782  isoid  5801  isoini  5809  resoprab2  5962  dfoprab3  6182  cnvoprab  6225  nnacan  6503  nnmcan  6510  isotilem  6995  eqinfti  7009  inflbti  7013  infglbti  7014  djuf1olem  7042  dfmpq2  7329  axsuploc  8004  div4p1lem1div2  9143  ztri3or  9267  nn0ind-raph  9341  zindd  9342  qreccl  9613  elpq  9619  iooshf  9921  fzofzim  10156  elfzomelpfzo  10199  zmodid2  10320  q2submod  10353  modfzo0difsn  10363  frec2uzltd  10371  frec2uzled  10397  prhash2ex  10755  iserex  11313  prodrbdc  11548  reef11  11673  absdvdsb  11782  dvdsabsb  11783  modmulconst  11796  dvdsadd  11809  dvdsabseq  11818  odd2np1  11843  mod2eq0even  11848  oddnn02np1  11850  oddge22np1  11851  evennn02n  11852  evennn2n  11853  zeo5  11858  gcdass  11981  lcmdvds  12044  lcmass  12050  divgcdcoprm0  12066  divgcdcoprmex  12067  1nprm  12079  dvdsnprmd  12090  isevengcd2  12123  m1dvdsndvds  12213