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  con2bidc  882  con1biidc  884  con2biidc  886  pm4.63dc  893  pm4.64dc  907  pm5.55dc  920  baibr  927  baibd  930  rbaibd  931  pm5.75  970  ninba  980  xor3dc  1431  3impexpbicomi  1484  cbvexv1  1800  cbvexh  1803  sbequ12r  1820  sbco  2021  sbcomxyyz  2025  sbal1yz  2054  cbvab  2355  nnedc  2407  necon3bbid  2442  necon2abiidc  2466  necon2bbiidc  2467  sbralie  2785  gencbvex  2850  gencbval  2852  sbhypf  2853  clel3g  2940  reu8  3002  sbceq2a  3042  sbcco2  3054  reu8nf  3113  sbcsng  3728  ssdifsn  3801  opabid  4350  soeq2  4413  tfisi  4685  posng  4798  xpiindim  4867  fvopab6  5743  fconstfvm  5872  cbvfo  5926  cbvexfo  5927  f1eqcocnv  5932  isoid  5951  isoini  5959  riotaeqimp  5996  resoprab2  6118  dfoprab3  6354  cnvoprab  6399  nnacan  6680  nnmcan  6687  isotilem  7205  eqinfti  7219  inflbti  7223  infglbti  7224  djuf1olem  7252  dfmpq2  7575  axsuploc  8252  div4p1lem1div2  9398  ztri3or  9522  nn0ind-raph  9597  zindd  9598  qreccl  9876  elpq  9883  iooshf  10187  fzofzim  10428  elfzomelpfzo  10477  zmodid2  10615  q2submod  10648  modfzo0difsn  10658  frec2uzltd  10666  frec2uzled  10692  prhash2ex  11074  swrd0g  11245  pfxn0  11273  swrdswrd  11290  pfxccat3  11319  iserex  11904  prodrbdc  12140  reef11  12265  absdvdsb  12375  dvdsabsb  12376  modmulconst  12389  dvdsadd  12402  dvdsabseq  12413  odd2np1  12439  mod2eq0even  12444  oddnn02np1  12446  oddge22np1  12447  evennn02n  12448  evennn2n  12449  zeo5  12454  gcdass  12591  lcmdvds  12656  lcmass  12662  divgcdcoprm0  12678  divgcdcoprmex  12679  1nprm  12691  dvdsnprmd  12702  isevengcd2  12735  m1dvdsndvds  12826  sgrppropd  13501  issubm2  13561  rngpropd  13974  rhmf1o  14188  isrim  14189  2lgslem1a  15823  edg0iedg0g  15923  uhgreq12g  15933  uhgrvtxedgiedgb  16000  edg0usgr  16104  umgrclwwlkge2  16259  isclwwlknx  16273  clwwlknonel  16289  clwwlknun  16298