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  bitr2id  192  bitr2di  196  pm5.5  241  anabs5  563  con2bidc  865  con1biidc  867  con2biidc  869  pm4.63dc  876  pm4.64dc  890  pm5.55dc  903  baibr  910  baibd  913  rbaibd  914  pm4.55dc  928  anordc  946  pm5.75  952  ninba  962  xor3dc  1377  3impexpbicomi  1427  cbvexv1  1740  cbvexh  1743  sbequ12r  1760  sbco  1956  sbcomxyyz  1960  sbal1yz  1989  cbvab  2289  nnedc  2340  necon3bbid  2375  necon2abiidc  2399  necon2bbiidc  2400  sbralie  2709  gencbvex  2771  gencbval  2773  sbhypf  2774  clel3g  2859  reu8  2921  sbceq2a  2960  sbcco2  2972  sbcsng  3634  ssdifsn  3703  opabid  4234  soeq2  4293  tfisi  4563  posng  4675  xpiindim  4740  fvopab6  5581  fconstfvm  5702  cbvfo  5752  cbvexfo  5753  f1eqcocnv  5758  isoid  5777  isoini  5785  resoprab2  5935  dfoprab3  6156  cnvoprab  6198  nnacan  6476  nnmcan  6483  isotilem  6967  eqinfti  6981  inflbti  6985  infglbti  6986  djuf1olem  7014  dfmpq2  7292  axsuploc  7967  div4p1lem1div2  9106  ztri3or  9230  nn0ind-raph  9304  zindd  9305  qreccl  9576  elpq  9582  iooshf  9884  fzofzim  10119  elfzomelpfzo  10162  zmodid2  10283  q2submod  10316  modfzo0difsn  10326  frec2uzltd  10334  frec2uzled  10360  prhash2ex  10718  iserex  11276  prodrbdc  11511  reef11  11636  absdvdsb  11745  dvdsabsb  11746  modmulconst  11759  dvdsadd  11772  dvdsabseq  11781  odd2np1  11806  mod2eq0even  11811  oddnn02np1  11813  oddge22np1  11814  evennn02n  11815  evennn2n  11816  zeo5  11821  gcdass  11944  lcmdvds  12007  lcmass  12013  divgcdcoprm0  12029  divgcdcoprmex  12030  1nprm  12042  dvdsnprmd  12053  isevengcd2  12086  m1dvdsndvds  12176