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  575  annotanannot  676  con2bidc  883  con1biidc  885  con2biidc  887  pm4.63dc  894  pm4.64dc  908  pm5.55dc  921  baibr  928  baibd  931  rbaibd  932  pm5.75  971  ninba  981  xor3dc  1432  3impexpbicomi  1485  cbvexv1  1801  cbvexh  1804  sbequ12r  1821  sbco  2024  sbcomxyyz  2028  sbal1yz  2057  cbvab  2360  eqabcdv  2366  nnedc  2419  necon3bbid  2454  necon2abiidc  2478  necon2bbiidc  2479  sbralie  2798  gencbvex  2863  gencbval  2865  sbhypf  2866  clel3g  2954  reu8  3016  sbceq2a  3056  sbcco2  3068  reu8nf  3127  sbcsng  3753  ssdifsn  3826  opabid  4379  soeq2  4442  tfisi  4714  posng  4827  xpiindim  4897  fvopab6  5779  fconstfvm  5907  cbvfo  5964  cbvexfo  5965  f1eqcocnv  5970  isoid  5989  isoini  5997  riotaeqimp  6036  resoprab2  6158  dfoprab3  6398  cnvoprab  6443  nnacan  6758  nnmcan  6765  mapsnd  6936  funisfsupp  7257  suppeqfsuppbi  7261  isotilem  7310  eqinfti  7324  inflbti  7328  infglbti  7329  djuf1olem  7357  dfmpq2  7686  axsuploc  8362  div4p1lem1div2  9512  ztri3or  9640  nn0ind-raph  9716  zindd  9717  qreccl  9995  elpq  10002  iooshf  10307  fzofzim  10552  elfzomelpfzo  10601  zmodid2  10741  q2submod  10774  modfzo0difsn  10784  frec2uzltd  10792  frec2uzled  10818  prhash2ex  11202  swrd0g  11380  pfxn0  11408  swrdswrd  11425  pfxccat3  11454  iserex  12053  prodrbdc  12289  reef11  12414  absdvdsb  12524  dvdsabsb  12525  modmulconst  12538  dvdsadd  12551  dvdsabseq  12562  odd2np1  12588  mod2eq0even  12593  oddnn02np1  12595  oddge22np1  12596  evennn02n  12597  evennn2n  12598  zeo5  12603  gcdass  12740  lcmdvds  12805  lcmass  12811  divgcdcoprm0  12827  divgcdcoprmex  12828  1nprm  12840  dvdsnprmd  12851  isevengcd2  12884  m1dvdsndvds  12975  sgrppropd  13680  issubm2  13732  rngpropd  14198  rhmf1o  14417  isrim  14418  2lgslem1a  16091  edg0iedg0g  16191  uhgreq12g  16201  uhgrvtxedgiedgb  16268  edg0usgr  16372  umgrclwwlkge2  16527  isclwwlknx  16541  clwwlknonel  16557  clwwlknun  16566