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  877  con1biidc  879  con2biidc  881  pm4.63dc  888  pm4.64dc  902  pm5.55dc  915  baibr  922  baibd  925  rbaibd  926  pm5.75  965  ninba  975  xor3dc  1407  3impexpbicomi  1459  cbvexv1  1775  cbvexh  1778  sbequ12r  1795  sbco  1996  sbcomxyyz  2000  sbal1yz  2029  cbvab  2329  nnedc  2381  necon3bbid  2416  necon2abiidc  2440  necon2bbiidc  2441  sbralie  2756  gencbvex  2819  gencbval  2821  sbhypf  2822  clel3g  2907  reu8  2969  sbceq2a  3009  sbcco2  3021  sbcsng  3692  ssdifsn  3761  opabid  4302  soeq2  4363  tfisi  4635  posng  4747  xpiindim  4815  fvopab6  5676  fconstfvm  5802  cbvfo  5854  cbvexfo  5855  f1eqcocnv  5860  isoid  5879  isoini  5887  resoprab2  6042  dfoprab3  6277  cnvoprab  6320  nnacan  6598  nnmcan  6605  isotilem  7108  eqinfti  7122  inflbti  7126  infglbti  7127  djuf1olem  7155  dfmpq2  7468  axsuploc  8145  div4p1lem1div2  9291  ztri3or  9415  nn0ind-raph  9490  zindd  9491  qreccl  9763  elpq  9770  iooshf  10074  fzofzim  10312  elfzomelpfzo  10360  zmodid2  10497  q2submod  10530  modfzo0difsn  10540  frec2uzltd  10548  frec2uzled  10574  prhash2ex  10954  swrd0g  11113  iserex  11650  prodrbdc  11885  reef11  12010  absdvdsb  12120  dvdsabsb  12121  modmulconst  12134  dvdsadd  12147  dvdsabseq  12158  odd2np1  12184  mod2eq0even  12189  oddnn02np1  12191  oddge22np1  12192  evennn02n  12193  evennn2n  12194  zeo5  12199  gcdass  12336  lcmdvds  12401  lcmass  12407  divgcdcoprm0  12423  divgcdcoprmex  12424  1nprm  12436  dvdsnprmd  12447  isevengcd2  12480  m1dvdsndvds  12571  sgrppropd  13245  issubm2  13305  rngpropd  13717  rhmf1o  13930  isrim  13931  2lgslem1a  15565