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  575  annotanannot  676  con2bidc  883  con1biidc  885  con2biidc  887  pm4.63dc  894  pm4.64dc  908  pm5.55dc  921  baibr  928  baibd  931  rbaibd  932  pm5.75  971  ninba  981  xor3dc  1432  3impexpbicomi  1485  cbvexv1  1801  cbvexh  1804  sbequ12r  1821  sbco  2022  sbcomxyyz  2026  sbal1yz  2055  cbvab  2358  eqabcdv  2364  nnedc  2417  necon3bbid  2452  necon2abiidc  2476  necon2bbiidc  2477  sbralie  2796  gencbvex  2861  gencbval  2863  sbhypf  2864  clel3g  2951  reu8  3013  sbceq2a  3053  sbcco2  3065  reu8nf  3124  sbcsng  3748  ssdifsn  3821  opabid  4374  soeq2  4437  tfisi  4709  posng  4822  xpiindim  4892  fvopab6  5774  fconstfvm  5902  cbvfo  5958  cbvexfo  5959  f1eqcocnv  5964  isoid  5983  isoini  5991  riotaeqimp  6028  resoprab2  6150  dfoprab3  6385  cnvoprab  6430  nnacan  6745  nnmcan  6752  mapsnd  6923  funisfsupp  7244  suppeqfsuppbi  7248  isotilem  7297  eqinfti  7311  inflbti  7315  infglbti  7316  djuf1olem  7344  dfmpq2  7670  axsuploc  8346  div4p1lem1div2  9492  ztri3or  9620  nn0ind-raph  9695  zindd  9696  qreccl  9974  elpq  9981  iooshf  10285  fzofzim  10527  elfzomelpfzo  10576  zmodid2  10714  q2submod  10747  modfzo0difsn  10757  frec2uzltd  10765  frec2uzled  10791  prhash2ex  11174  swrd0g  11352  pfxn0  11380  swrdswrd  11397  pfxccat3  11426  iserex  12024  prodrbdc  12260  reef11  12385  absdvdsb  12495  dvdsabsb  12496  modmulconst  12509  dvdsadd  12522  dvdsabseq  12533  odd2np1  12559  mod2eq0even  12564  oddnn02np1  12566  oddge22np1  12567  evennn02n  12568  evennn2n  12569  zeo5  12574  gcdass  12711  lcmdvds  12776  lcmass  12782  divgcdcoprm0  12798  divgcdcoprmex  12799  1nprm  12811  dvdsnprmd  12822  isevengcd2  12855  m1dvdsndvds  12946  sgrppropd  13626  issubm2  13686  rngpropd  14099  rhmf1o  14313  isrim  14314  2lgslem1a  15961  edg0iedg0g  16061  uhgreq12g  16071  uhgrvtxedgiedgb  16138  edg0usgr  16242  umgrclwwlkge2  16397  isclwwlknx  16411  clwwlknonel  16427  clwwlknun  16436