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  2721  gencbvex  2783  gencbval  2785  sbhypf  2786  clel3g  2871  reu8  2933  sbceq2a  2973  sbcco2  2985  sbcsng  3651  ssdifsn  3720  opabid  4257  soeq2  4316  tfisi  4586  posng  4698  xpiindim  4764  fvopab6  5612  fconstfvm  5734  cbvfo  5785  cbvexfo  5786  f1eqcocnv  5791  isoid  5810  isoini  5818  resoprab2  5971  dfoprab3  6191  cnvoprab  6234  nnacan  6512  nnmcan  6519  isotilem  7004  eqinfti  7018  inflbti  7022  infglbti  7023  djuf1olem  7051  dfmpq2  7353  axsuploc  8028  div4p1lem1div2  9170  ztri3or  9294  nn0ind-raph  9368  zindd  9369  qreccl  9640  elpq  9646  iooshf  9950  fzofzim  10185  elfzomelpfzo  10228  zmodid2  10349  q2submod  10382  modfzo0difsn  10392  frec2uzltd  10400  frec2uzled  10426  prhash2ex  10784  iserex  11342  prodrbdc  11577  reef11  11702  absdvdsb  11811  dvdsabsb  11812  modmulconst  11825  dvdsadd  11838  dvdsabseq  11847  odd2np1  11872  mod2eq0even  11877  oddnn02np1  11879  oddge22np1  11880  evennn02n  11881  evennn2n  11882  zeo5  11887  gcdass  12010  lcmdvds  12073  lcmass  12079  divgcdcoprm0  12095  divgcdcoprmex  12096  1nprm  12108  dvdsnprmd  12119  isevengcd2  12152  m1dvdsndvds  12242  issubm2  12858