Theorem bicomd 140

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 139	. 2 |- ( ( ps <-> ch ) <-> ( ch <-> ps ) )
3	1, 2	sylib 121	1 |- ( ph -> ( ch <-> ps ) )

Syntax hints:   -> wi 4   <-> wb 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  impbid2  142  syl5ibr  155  ibir  176  bitr2d  188  bitr3d  189  bitr4d  190  syl5rbb  192  syl6rbb  196  pm5.5  241  anabs5  562  con2bidc  860  con1biidc  862  con2biidc  864  pm4.63dc  871  pm4.64dc  885  pm5.55dc  898  baibr  905  baibd  908  rbaibd  909  pm4.55dc  922  anordc  940  pm5.75  946  ninba  956  xor3dc  1365  3impexpbicomi  1415  cbvexh  1728  sbequ12r  1745  sbco  1939  sbcomxyyz  1943  sbal1yz  1974  cbvab  2261  nnedc  2311  necon3bbid  2346  necon2abiidc  2370  necon2bbiidc  2371  sbralie  2665  gencbvex  2727  gencbval  2729  sbhypf  2730  clel3g  2814  reu8  2875  sbceq2a  2914  sbcco2  2926  sbcsng  3577  ssdifsn  3646  opabid  4174  soeq2  4233  tfisi  4496  posng  4606  xpiindim  4671  fvopab6  5510  fconstfvm  5631  cbvfo  5679  cbvexfo  5680  f1eqcocnv  5685  isoid  5704  isoini  5712  resoprab2  5861  dfoprab3  6082  cnvoprab  6124  nnacan  6401  nnmcan  6408  isotilem  6886  eqinfti  6900  inflbti  6904  infglbti  6905  djuf1olem  6931  dfmpq2  7156  axsuploc  7830  div4p1lem1div2  8966  ztri3or  9090  nn0ind-raph  9161  zindd  9162  qreccl  9427  iooshf  9728  fzofzim  9958  elfzomelpfzo  10001  zmodid2  10118  q2submod  10151  modfzo0difsn  10161  frec2uzltd  10169  frec2uzled  10195  prhash2ex  10548  iserex  11101  prodrbdc  11336  reef11  11395  absdvdsb  11500  dvdsabsb  11501  modmulconst  11514  dvdsadd  11525  dvdsabseq  11534  odd2np1  11559  mod2eq0even  11564  oddnn02np1  11566  oddge22np1  11567  evennn02n  11568  evennn2n  11569  zeo5  11574  gcdass  11692  lcmdvds  11749  lcmass  11755  divgcdcoprm0  11771  divgcdcoprmex  11772  1nprm  11784  dvdsnprmd  11795  isevengcd2  11825  bj-indeq  13116