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  876  con1biidc  878  con2biidc  880  pm4.63dc  887  pm4.64dc  901  pm5.55dc  914  baibr  921  baibd  924  rbaibd  925  pm5.75  964  ninba  974  xor3dc  1398  3impexpbicomi  1450  cbvexv1  1766  cbvexh  1769  sbequ12r  1786  sbco  1987  sbcomxyyz  1991  sbal1yz  2020  cbvab  2320  nnedc  2372  necon3bbid  2407  necon2abiidc  2431  necon2bbiidc  2432  sbralie  2747  gencbvex  2810  gencbval  2812  sbhypf  2813  clel3g  2898  reu8  2960  sbceq2a  3000  sbcco2  3012  sbcsng  3681  ssdifsn  3750  opabid  4290  soeq2  4351  tfisi  4623  posng  4735  xpiindim  4803  fvopab6  5658  fconstfvm  5780  cbvfo  5832  cbvexfo  5833  f1eqcocnv  5838  isoid  5857  isoini  5865  resoprab2  6019  dfoprab3  6249  cnvoprab  6292  nnacan  6570  nnmcan  6577  isotilem  7072  eqinfti  7086  inflbti  7090  infglbti  7091  djuf1olem  7119  dfmpq2  7422  axsuploc  8099  div4p1lem1div2  9245  ztri3or  9369  nn0ind-raph  9443  zindd  9444  qreccl  9716  elpq  9723  iooshf  10027  fzofzim  10264  elfzomelpfzo  10307  zmodid2  10444  q2submod  10477  modfzo0difsn  10487  frec2uzltd  10495  frec2uzled  10521  prhash2ex  10901  iserex  11504  prodrbdc  11739  reef11  11864  absdvdsb  11974  dvdsabsb  11975  modmulconst  11988  dvdsadd  12001  dvdsabseq  12012  odd2np1  12038  mod2eq0even  12043  oddnn02np1  12045  oddge22np1  12046  evennn02n  12047  evennn2n  12048  zeo5  12053  gcdass  12182  lcmdvds  12247  lcmass  12253  divgcdcoprm0  12269  divgcdcoprmex  12270  1nprm  12282  dvdsnprmd  12293  isevengcd2  12326  m1dvdsndvds  12417  sgrppropd  13056  issubm2  13105  rngpropd  13511  rhmf1o  13724  isrim  13725  2lgslem1a  15329