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  annotanannot  676  con2bidc  883  con1biidc  885  con2biidc  887  pm4.63dc  894  pm4.64dc  908  pm5.55dc  921  baibr  928  baibd  931  rbaibd  932  pm5.75  971  ninba  981  xor3dc  1432  3impexpbicomi  1485  cbvexv1  1800  cbvexh  1803  sbequ12r  1820  sbco  2021  sbcomxyyz  2025  sbal1yz  2054  cbvab  2356  nnedc  2408  necon3bbid  2443  necon2abiidc  2467  necon2bbiidc  2468  sbralie  2786  gencbvex  2851  gencbval  2853  sbhypf  2854  clel3g  2941  reu8  3003  sbceq2a  3043  sbcco2  3055  reu8nf  3114  sbcsng  3732  ssdifsn  3805  opabid  4356  soeq2  4419  tfisi  4691  posng  4804  xpiindim  4873  fvopab6  5752  fconstfvm  5880  cbvfo  5936  cbvexfo  5937  f1eqcocnv  5942  isoid  5961  isoini  5969  riotaeqimp  6006  resoprab2  6128  dfoprab3  6363  cnvoprab  6408  nnacan  6723  nnmcan  6730  funisfsupp  7216  suppeqfsuppbi  7220  isotilem  7265  eqinfti  7279  inflbti  7283  infglbti  7284  djuf1olem  7312  dfmpq2  7635  axsuploc  8311  div4p1lem1div2  9457  ztri3or  9583  nn0ind-raph  9658  zindd  9659  qreccl  9937  elpq  9944  iooshf  10248  fzofzim  10490  elfzomelpfzo  10539  zmodid2  10677  q2submod  10710  modfzo0difsn  10720  frec2uzltd  10728  frec2uzled  10754  prhash2ex  11136  swrd0g  11307  pfxn0  11335  swrdswrd  11352  pfxccat3  11381  iserex  11979  prodrbdc  12215  reef11  12340  absdvdsb  12450  dvdsabsb  12451  modmulconst  12464  dvdsadd  12477  dvdsabseq  12488  odd2np1  12514  mod2eq0even  12519  oddnn02np1  12521  oddge22np1  12522  evennn02n  12523  evennn2n  12524  zeo5  12529  gcdass  12666  lcmdvds  12731  lcmass  12737  divgcdcoprm0  12753  divgcdcoprmex  12754  1nprm  12766  dvdsnprmd  12777  isevengcd2  12810  m1dvdsndvds  12901  sgrppropd  13576  issubm2  13636  rngpropd  14049  rhmf1o  14263  isrim  14264  2lgslem1a  15907  edg0iedg0g  16007  uhgreq12g  16017  uhgrvtxedgiedgb  16084  edg0usgr  16188  umgrclwwlkge2  16343  isclwwlknx  16357  clwwlknonel  16373  clwwlknun  16382