Theorem bicomd 192

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 191	. 2 ⊢ ((ψ ↔ χ) ↔ (χ ↔ ψ))
3	1, 2	sylib 188	1 ⊢ (φ → (χ ↔ ψ))

Syntax hints:   → wi 4   ↔ wb 176

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

This theorem depends on definitions:  df-bi 177

This theorem is referenced by:  impbid2  195  syl5ibr  212  ibir  233  bitr2d  245  bitr3d  246  bitr4d  247  syl5rbb  249  syl6rbb  253  con1bid  320  pm5.5  326  anabs5  784  pm5.55  867  pm5.54  870  baibr  872  baibd  875  rbaibd  876  pm5.75  903  ninba  927  3impexpbicomi  1368  cad1  1398  sbequ12r  1920  sbco  2083  sbco2  2086  cbvab  2471  necon3bbid  2550  necon4bbid  2581  ralcom2  2775  sbralie  2848  gencbvex  2901  sbhypf  2904  clel3g  2976  reu8  3032  sbceq2a  3057  sbcco2  3069  r19.9rzv  3644  sbcsng  3783  opkelcokg  4261  elssetkg  4269  nnsucelrlem2  4425  opabid  4695  fconstfv  5456  isoid  5490  isoini  5497  funsi  5520  resoprab2  5582  nmembers1lem3  6270  epelcres  6328