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  573  con2bidc  875  con1biidc  877  con2biidc  879  pm4.63dc  886  pm4.64dc  900  pm5.55dc  913  baibr  920  baibd  923  rbaibd  924  pm4.55dc  938  anordc  956  pm5.75  962  ninba  972  xor3dc  1387  3impexpbicomi  1439  cbvexv1  1752  cbvexh  1755  sbequ12r  1772  sbco  1968  sbcomxyyz  1972  sbal1yz  2001  cbvab  2301  nnedc  2352  necon3bbid  2387  necon2abiidc  2411  necon2bbiidc  2412  sbralie  2722  gencbvex  2784  gencbval  2786  sbhypf  2787  clel3g  2872  reu8  2934  sbceq2a  2974  sbcco2  2986  sbcsng  3652  ssdifsn  3721  opabid  4258  soeq2  4317  tfisi  4587  posng  4699  xpiindim  4765  fvopab6  5613  fconstfvm  5735  cbvfo  5786  cbvexfo  5787  f1eqcocnv  5792  isoid  5811  isoini  5819  resoprab2  5972  dfoprab3  6192  cnvoprab  6235  nnacan  6513  nnmcan  6520  isotilem  7005  eqinfti  7019  inflbti  7023  infglbti  7024  djuf1olem  7052  dfmpq2  7354  axsuploc  8030  div4p1lem1div2  9172  ztri3or  9296  nn0ind-raph  9370  zindd  9371  qreccl  9642  elpq  9648  iooshf  9952  fzofzim  10188  elfzomelpfzo  10231  zmodid2  10352  q2submod  10385  modfzo0difsn  10395  frec2uzltd  10403  frec2uzled  10429  prhash2ex  10789  iserex  11347  prodrbdc  11582  reef11  11707  absdvdsb  11816  dvdsabsb  11817  modmulconst  11830  dvdsadd  11843  dvdsabseq  11853  odd2np1  11878  mod2eq0even  11883  oddnn02np1  11885  oddge22np1  11886  evennn02n  11887  evennn2n  11888  zeo5  11893  gcdass  12016  lcmdvds  12079  lcmass  12085  divgcdcoprm0  12101  divgcdcoprmex  12102  1nprm  12114  dvdsnprmd  12125  isevengcd2  12158  m1dvdsndvds  12248  issubm2  12864