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  8029  div4p1lem1div2  9171  ztri3or  9295  nn0ind-raph  9369  zindd  9370  qreccl  9641  elpq  9647  iooshf  9951  fzofzim  10187  elfzomelpfzo  10230  zmodid2  10351  q2submod  10384  modfzo0difsn  10394  frec2uzltd  10402  frec2uzled  10428  prhash2ex  10788  iserex  11346  prodrbdc  11581  reef11  11706  absdvdsb  11815  dvdsabsb  11816  modmulconst  11829  dvdsadd  11842  dvdsabseq  11852  odd2np1  11877  mod2eq0even  11882  oddnn02np1  11884  oddge22np1  11885  evennn02n  11886  evennn2n  11887  zeo5  11892  gcdass  12015  lcmdvds  12078  lcmass  12084  divgcdcoprm0  12100  divgcdcoprmex  12101  1nprm  12113  dvdsnprmd  12124  isevengcd2  12157  m1dvdsndvds  12247  issubm2  12863