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  573  con2bidc  880  con1biidc  882  con2biidc  884  pm4.63dc  891  pm4.64dc  905  pm5.55dc  918  baibr  925  baibd  928  rbaibd  929  pm5.75  968  ninba  978  xor3dc  1429  3impexpbicomi  1482  cbvexv1  1798  cbvexh  1801  sbequ12r  1818  sbco  2019  sbcomxyyz  2023  sbal1yz  2052  cbvab  2353  nnedc  2405  necon3bbid  2440  necon2abiidc  2464  necon2bbiidc  2465  sbralie  2783  gencbvex  2848  gencbval  2850  sbhypf  2851  clel3g  2938  reu8  3000  sbceq2a  3040  sbcco2  3052  reu8nf  3111  sbcsng  3726  ssdifsn  3799  opabid  4348  soeq2  4411  tfisi  4683  posng  4796  xpiindim  4865  fvopab6  5739  fconstfvm  5867  cbvfo  5921  cbvexfo  5922  f1eqcocnv  5927  isoid  5946  isoini  5954  riotaeqimp  5991  resoprab2  6113  dfoprab3  6349  cnvoprab  6394  nnacan  6675  nnmcan  6682  isotilem  7196  eqinfti  7210  inflbti  7214  infglbti  7215  djuf1olem  7243  dfmpq2  7565  axsuploc  8242  div4p1lem1div2  9388  ztri3or  9512  nn0ind-raph  9587  zindd  9588  qreccl  9866  elpq  9873  iooshf  10177  fzofzim  10417  elfzomelpfzo  10466  zmodid2  10604  q2submod  10637  modfzo0difsn  10647  frec2uzltd  10655  frec2uzled  10681  prhash2ex  11063  swrd0g  11231  pfxn0  11259  swrdswrd  11276  pfxccat3  11305  iserex  11890  prodrbdc  12125  reef11  12250  absdvdsb  12360  dvdsabsb  12361  modmulconst  12374  dvdsadd  12387  dvdsabseq  12398  odd2np1  12424  mod2eq0even  12429  oddnn02np1  12431  oddge22np1  12432  evennn02n  12433  evennn2n  12434  zeo5  12439  gcdass  12576  lcmdvds  12641  lcmass  12647  divgcdcoprm0  12663  divgcdcoprmex  12664  1nprm  12676  dvdsnprmd  12687  isevengcd2  12720  m1dvdsndvds  12811  sgrppropd  13486  issubm2  13546  rngpropd  13958  rhmf1o  14172  isrim  14173  2lgslem1a  15807  edg0iedg0g  15907  uhgreq12g  15917  uhgrvtxedgiedgb  15982  edg0usgr  16086  umgrclwwlkge2  16197  isclwwlknx  16211  clwwlknonel  16227  clwwlknun  16236