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  9509  ztri3or  9637  nn0ind-raph  9713  zindd  9714  qreccl  9992  elpq  9999  iooshf  10304  fzofzim  10549  elfzomelpfzo  10598  zmodid2  10738  q2submod  10771  modfzo0difsn  10781  frec2uzltd  10789  frec2uzled  10815  prhash2ex  11199  swrd0g  11377  pfxn0  11405  swrdswrd  11422  pfxccat3  11451  iserex  12049  prodrbdc  12285  reef11  12410  absdvdsb  12520  dvdsabsb  12521  modmulconst  12534  dvdsadd  12547  dvdsabseq  12558  odd2np1  12584  mod2eq0even  12589  oddnn02np1  12591  oddge22np1  12592  evennn02n  12593  evennn2n  12594  zeo5  12599  gcdass  12736  lcmdvds  12801  lcmass  12807  divgcdcoprm0  12823  divgcdcoprmex  12824  1nprm  12836  dvdsnprmd  12847  isevengcd2  12880  m1dvdsndvds  12971  sgrppropd  13676  issubm2  13728  rngpropd  14194  rhmf1o  14413  isrim  14414  2lgslem1a  16087  edg0iedg0g  16187  uhgreq12g  16197  uhgrvtxedgiedgb  16264  edg0usgr  16368  umgrclwwlkge2  16523  isclwwlknx  16537  clwwlknonel  16553  clwwlknun  16562