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  4398  soeq2  4461  tfisi  4734  posng  4847  xpiindim  4917  fvopab6  5805  fconstfvm  5933  cbvfo  5991  cbvexfo  5992  f1eqcocnv  5997  isoid  6016  isoini  6024  riotaeqimp  6063  resoprab2  6185  dfoprab3  6425  cnvoprab  6470  nnacan  6785  nnmcan  6792  mapsnd  6970  funisfsupp  7291  suppeqfsuppbi  7295  isotilem  7346  eqinfti  7360  inflbti  7364  infglbti  7365  djuf1olem  7393  dfmpq2  7722  axsuploc  8398  div4p1lem1div2  9563  ztri3or  9691  nn0ind-raph  9767  zindd  9768  qreccl  10051  elpq  10059  iooshf  10364  fzofzim  10610  elfzomelpfzo  10659  zmodid2  10802  q2submod  10835  modfzo0difsn  10845  frec2uzltd  10853  frec2uzled  10879  prhash2ex  11264  hashf1lem2  11300  swrd0g  11446  pfxn0  11474  swrdswrd  11491  pfxccat3  11520  iserex  12121  prodrbdc  12357  reef11  12482  absdvdsb  12592  dvdsabsb  12593  modmulconst  12606  dvdsadd  12619  dvdsabseq  12630  odd2np1  12656  mod2eq0even  12661  oddnn02np1  12663  oddge22np1  12664  evennn02n  12665  evennn2n  12666  zeo5  12671  gcdass  12808  lcmdvds  12873  lcmass  12879  divgcdcoprm0  12895  divgcdcoprmex  12896  1nprm  12908  dvdsnprmd  12919  isevengcd2  12953  m1dvdsndvds  13047  sgrppropd  13777  issubm2  13829  rngpropd  14303  rhmf1o  14524  isrim  14525  2lgslem1a  16305  edg0iedg0g  16405  uhgreq12g  16415  uhgrvtxedgiedgb  16482  edg0usgr  16586  umgrclwwlkge2  16741  isclwwlknx  16755  clwwlknonel  16771  clwwlknun  16780  ralrals  17247  rexrals  17248  ralals  17253  rexals  17254