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  bitr2di  196  pm5.5  241  anabs5  563  con2bidc  861  con1biidc  863  con2biidc  865  pm4.63dc  872  pm4.64dc  886  pm5.55dc  899  baibr  906  baibd  909  rbaibd  910  pm4.55dc  923  anordc  941  pm5.75  947  ninba  957  xor3dc  1369  3impexpbicomi  1419  cbvexv1  1732  cbvexh  1735  sbequ12r  1752  sbco  1948  sbcomxyyz  1952  sbal1yz  1981  cbvab  2281  nnedc  2332  necon3bbid  2367  necon2abiidc  2391  necon2bbiidc  2392  sbralie  2696  gencbvex  2758  gencbval  2760  sbhypf  2761  clel3g  2846  reu8  2908  sbceq2a  2947  sbcco2  2959  sbcsng  3618  ssdifsn  3687  opabid  4216  soeq2  4275  tfisi  4544  posng  4655  xpiindim  4720  fvopab6  5561  fconstfvm  5682  cbvfo  5730  cbvexfo  5731  f1eqcocnv  5736  isoid  5755  isoini  5763  resoprab2  5912  dfoprab3  6133  cnvoprab  6175  nnacan  6452  nnmcan  6459  isotilem  6942  eqinfti  6956  inflbti  6960  infglbti  6961  djuf1olem  6987  dfmpq2  7258  axsuploc  7933  div4p1lem1div2  9069  ztri3or  9193  nn0ind-raph  9264  zindd  9265  qreccl  9533  elpq  9539  iooshf  9838  fzofzim  10069  elfzomelpfzo  10112  zmodid2  10233  q2submod  10266  modfzo0difsn  10276  frec2uzltd  10284  frec2uzled  10310  prhash2ex  10665  iserex  11218  prodrbdc  11453  reef11  11578  absdvdsb  11686  dvdsabsb  11687  modmulconst  11700  dvdsadd  11711  dvdsabseq  11720  odd2np1  11745  mod2eq0even  11750  oddnn02np1  11752  oddge22np1  11753  evennn02n  11754  evennn2n  11755  zeo5  11760  gcdass  11879  lcmdvds  11936  lcmass  11942  divgcdcoprm0  11958  divgcdcoprmex  11959  1nprm  11971  dvdsnprmd  11982  isevengcd2  12012  bj-indeq  13464