Theorem bicomd 192

Description: Commute two sides of a biconditional in a deduction. (Contributed by NM, 5-Aug-1993.)

Hypothesis

Ref	Expression
bicomd.1	|- (ph -> (ps <-> ch))

Assertion

Ref	Expression
bicomd	|- (ph -> (ch <-> ps))

Proof of Theorem bicomd

Step	Hyp	Ref	Expression
1		bicomd.1	. 2 |- (ph -> (ps <-> ch))
2		bicom 191	. 2 |- ((ps <-> ch) <-> (ch <-> ps))
3	1, 2	sylib 188	1 |- (ph -> (ch <-> ps))

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  2472  necon3bbid  2551  necon4bbid  2582  ralcom2  2776  sbralie  2849  gencbvex  2902  sbhypf  2905  clel3g  2977  reu8  3033  sbceq2a  3058  sbcco2  3070  r19.9rzv  3645  sbcsng  3784  opkelcokg  4262  elssetkg  4270  nnsucelrlem2  4426  opabid  4696  fconstfv  5457  isoid  5491  isoini  5498  funsi  5521  resoprab2  5583  nmembers1lem3  6271  epelcres  6329