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  2847  gencbval  2849  sbhypf  2850  clel3g  2937  reu8  2999  sbceq2a  3039  sbcco2  3051  reu8nf  3110  sbcsng  3725  ssdifsn  3795  opabid  4343  soeq2  4406  tfisi  4678  posng  4790  xpiindim  4858  fvopab6  5730  fconstfvm  5856  cbvfo  5908  cbvexfo  5909  f1eqcocnv  5914  isoid  5933  isoini  5941  riotaeqimp  5978  resoprab2  6100  dfoprab3  6335  cnvoprab  6378  nnacan  6656  nnmcan  6663  isotilem  7169  eqinfti  7183  inflbti  7187  infglbti  7188  djuf1olem  7216  dfmpq2  7538  axsuploc  8215  div4p1lem1div2  9361  ztri3or  9485  nn0ind-raph  9560  zindd  9561  qreccl  9833  elpq  9840  iooshf  10144  fzofzim  10384  elfzomelpfzo  10432  zmodid2  10569  q2submod  10602  modfzo0difsn  10612  frec2uzltd  10620  frec2uzled  10646  prhash2ex  11026  swrd0g  11187  pfxn0  11215  swrdswrd  11232  pfxccat3  11261  iserex  11845  prodrbdc  12080  reef11  12205  absdvdsb  12315  dvdsabsb  12316  modmulconst  12329  dvdsadd  12342  dvdsabseq  12353  odd2np1  12379  mod2eq0even  12384  oddnn02np1  12386  oddge22np1  12387  evennn02n  12388  evennn2n  12389  zeo5  12394  gcdass  12531  lcmdvds  12596  lcmass  12602  divgcdcoprm0  12618  divgcdcoprmex  12619  1nprm  12631  dvdsnprmd  12642  isevengcd2  12675  m1dvdsndvds  12766  sgrppropd  13441  issubm2  13501  rngpropd  13913  rhmf1o  14126  isrim  14127  2lgslem1a  15761  edg0iedg0g  15860  uhgreq12g  15870  uhgrvtxedgiedgb  15935