Theorem bicomd 141

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

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

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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  impbid2  143  imbitrrid  156  ibir  177  bitr2d  189  bitr3d  190  bitr4d  191  bitr2id  193  bitr2di  197  pm5.5  242  anabs5  575  con2bidc  882  con1biidc  884  con2biidc  886  pm4.63dc  893  pm4.64dc  907  pm5.55dc  920  baibr  927  baibd  930  rbaibd  931  pm5.75  970  ninba  980  xor3dc  1431  3impexpbicomi  1484  cbvexv1  1800  cbvexh  1803  sbequ12r  1820  sbco  2021  sbcomxyyz  2025  sbal1yz  2054  cbvab  2355  nnedc  2407  necon3bbid  2442  necon2abiidc  2466  necon2bbiidc  2467  sbralie  2785  gencbvex  2850  gencbval  2852  sbhypf  2853  clel3g  2940  reu8  3002  sbceq2a  3042  sbcco2  3054  reu8nf  3113  sbcsng  3728  ssdifsn  3801  opabid  4350  soeq2  4413  tfisi  4685  posng  4798  xpiindim  4867  fvopab6  5743  fconstfvm  5872  cbvfo  5926  cbvexfo  5927  f1eqcocnv  5932  isoid  5951  isoini  5959  riotaeqimp  5996  resoprab2  6118  dfoprab3  6354  cnvoprab  6399  nnacan  6680  nnmcan  6687  isotilem  7205  eqinfti  7219  inflbti  7223  infglbti  7224  djuf1olem  7252  dfmpq2  7575  axsuploc  8252  div4p1lem1div2  9398  ztri3or  9522  nn0ind-raph  9597  zindd  9598  qreccl  9876  elpq  9883  iooshf  10187  fzofzim  10428  elfzomelpfzo  10477  zmodid2  10615  q2submod  10648  modfzo0difsn  10658  frec2uzltd  10666  frec2uzled  10692  prhash2ex  11074  swrd0g  11245  pfxn0  11273  swrdswrd  11290  pfxccat3  11319  iserex  11917  prodrbdc  12153  reef11  12278  absdvdsb  12388  dvdsabsb  12389  modmulconst  12402  dvdsadd  12415  dvdsabseq  12426  odd2np1  12452  mod2eq0even  12457  oddnn02np1  12459  oddge22np1  12460  evennn02n  12461  evennn2n  12462  zeo5  12467  gcdass  12604  lcmdvds  12669  lcmass  12675  divgcdcoprm0  12691  divgcdcoprmex  12692  1nprm  12704  dvdsnprmd  12715  isevengcd2  12748  m1dvdsndvds  12839  sgrppropd  13514  issubm2  13574  rngpropd  13987  rhmf1o  14201  isrim  14202  2lgslem1a  15836  edg0iedg0g  15936  uhgreq12g  15946  uhgrvtxedgiedgb  16013  edg0usgr  16117  umgrclwwlkge2  16272  isclwwlknx  16286  clwwlknonel  16302  clwwlknun  16311