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 ⊢ (𝜑 → (𝜒 ↔ 𝜓))

This proof depends on syntax axioms:   → wi 4   ↔ wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  impbid2  143  imbitrrid  156  ibir  177  bitr2d  189  bitr3d  190  bitr4d  191  bitr2id  193  bitr2di  197  pm5.5  242  anabs5  579  annotanannot  680  con2bidc  887  con1biidc  889  con2biidc  891  pm4.63dc  898  pm4.64dc  912  pm5.55dc  925  baibr  932  baibd  935  rbaibd  936  pm5.75  975  ninba  985  xor3dc  1436  3impexpbicomi  1489  cbvexv1  1805  cbvexh  1808  sbequ12r  1825  sbco  2028  sbcomxyyz  2032  sbal1yz  2061  cbvab  2364  eqabcdv  2370  nnedc  2425  necon3bbid  2460  necon2abiidc  2484  necon2bbiidc  2485  sbralie  2804  gencbvex  2869  gencbval  2871  sbhypf  2872  clel3g  2960  reu8  3022  sbceq2a  3062  sbcco2  3074  reu8nf  3133  sbcsng  3768  ssdifsn  3842  opabid  4400  soeq2  4463  tfisi  4736  posng  4849  xpiindim  4919  fvopab6  5808  fconstfvm  5936  cbvfo  5994  cbvexfo  5995  f1eqcocnv  6000  isoid  6019  isoini  6027  riotaeqimp  6066  resoprab2  6188  dfoprab3  6429  cnvoprab  6474  nnacan  6790  nnmcan  6797  mapsnd  6976  isotilem  7352  eqinfti  7366  inflbti  7370  infglbti  7371  djuf1olem  7399  dfmpq2  7728  axsuploc  8404  div4p1lem1div2  9570  ztri3or  9696  nn0ind-raph  9773  zindd  9774  qreccl  10057  elpq  10065  iooshf  10370  fzofzim  10616  elfzomelpfzo  10665  zmodid2  10809  q2submod  10842  modfzo0difsn  10852  frec2uzltd  10860  frec2uzled  10886  prhash2ex  11271  hashf1lem2  11307  swrd0g  11453  pfxn0  11481  swrdswrd  11498  pfxccat3  11527  iserex  12129  prodrbdc  12365  reef11  12490  absdvdsb  12600  dvdsabsb  12601  modmulconst  12614  dvdsadd  12627  dvdsabseq  12638  odd2np1  12664  mod2eq0even  12669  oddnn02np1  12671  oddge22np1  12672  evennn02n  12673  evennn2n  12674  zeo5  12679  gcdass  12816  lcmdvds  12881  lcmass  12887  divgcdcoprm0  12903  divgcdcoprmex  12904  1nprm  12916  dvdsnprmd  12927  isevengcd2  12961  m1dvdsndvds  13055  sgrppropd  13786  issubm2  13838  sscntz  14157  rngpropd  14360  rhmf1o  14583  isrim  14584  2lgslem1a  16429  edg0iedg0g  16529  uhgreq12g  16539  uhgrvtxedgiedgb  16606  edg0usgr  16710  umgrclwwlkge2  16865  isclwwlknx  16879  clwwlknonel  16895  clwwlknun  16904  ralrals  17373  rexrals  17374  ralals  17379  rexals  17380