Theorem bicomd 524

Description: Commute two sides of a biconditional in a deduction.

Hypothesis

Ref	Expression
bicomd.1	⊢ (φ → (ψ ↔ χ))

Assertion

Ref	Expression
bicomd	⊢ (φ → (χ ↔ ψ))

Proof of Theorem bicomd

Step	Hyp	Ref	Expression
1		bicomd.1	. 2 ⊢ (φ → (ψ ↔ χ))
2		bicom 523	. 2 ⊢ ((ψ ↔ χ) ↔ (χ ↔ ψ))
3	1, 2	sylib 196	1 ⊢ (φ → (χ ↔ ψ))

Syntax hints:   → wi 3   ↔ wb 144

This theorem is referenced by:  con1bid 530  bitr2d 532  bitr3d 533  bitr4d 534  syl5rbb 536  syl6rbb 540  ibir 596  pm5.54 687  baibr 690  pm5.5 737  bimsc1 755  ninba 774  sbco 1290  sbidm 1292  sbco2 1293  necon3bbid 1643  gencbvex 1884  clel3g 1938  moi2 1970  moi 1971  reu8 1982  sbhypf 1985  r19.9rzv 2403  ifboth 2429  iununi 2686  poeq2 2921  posn 2928  soeq2 2933  freq2 2953  tfinds2 3216  fconstfv 3963  isoid 4009  isoini 4014  isowe 4017  f1oweALT 4020  tfrlem5 4216  oaword 4319  oalimcl 4330  omword 4337  oeword 4353  nnaordex 4389  nnawordex 4390  pw2en 4587  carduni 5008  aleph11 5029  alephval3 5053  axrepndlem2 5099  lttri2 5667  xrlttri2 5709  muln0b 5849  lemul1 5973  lemul1OLD 5974  lt2msqi 6026  msq11i 6028  nn0ind-raph 6385  zindd 6386  rebtwnz 6394  qreccl 6412  qsqueeze 6420  iooshf 6522  om2uzlti 6661  2climnn 7305  2climnn0 7306  ef01tllem2OLD 7590  znnen 7714  gch-kn 7799  bastop1 7854  iscld2 7880  isopn2 7883  lmclimnn 8175  norm-i 9272  hoeq 9966  nmopgt0 10116  elnlfn 10132  irredi 10603  infi1 10735  fiiu 10738  cmpfun 10751  cnvref 10769  seqzp2 10918  cdrci 10994  hmph 11030  cnvhmph 11033  hmeogrp 11044  fillsb 11073  cnfilca 11088  rcfpfil 11095  isfuna 11288  subtr2 11396  cbvsbc 11398  ordiso 11426  omsubsdom 11442  compsub 11488  topbasfne 11560  limfilcf 11683  fcluscf 11724  resoprab2 11809  indexa 11845  sdc 11877  caushft 11916

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7

This theorem depends on definitions:  df-bi 145  df-an 223

Copyright terms: Public domain