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  880  con1biidc  882  con2biidc  884  pm4.63dc  891  pm4.64dc  905  pm5.55dc  918  baibr  925  baibd  928  rbaibd  929  pm5.75  968  ninba  978  xor3dc  1429  3impexpbicomi  1482  cbvexv1  1798  cbvexh  1801  sbequ12r  1818  sbco  2019  sbcomxyyz  2023  sbal1yz  2052  cbvab  2353  nnedc  2405  necon3bbid  2440  necon2abiidc  2464  necon2bbiidc  2465  sbralie  2783  gencbvex  2847  gencbval  2849  sbhypf  2850  clel3g  2937  reu8  2999  sbceq2a  3039  sbcco2  3051  reu8nf  3110  sbcsng  3725  ssdifsn  3796  opabid  4344  soeq2  4407  tfisi  4679  posng  4791  xpiindim  4859  fvopab6  5731  fconstfvm  5857  cbvfo  5909  cbvexfo  5910  f1eqcocnv  5915  isoid  5934  isoini  5942  riotaeqimp  5979  resoprab2  6101  dfoprab3  6337  cnvoprab  6380  nnacan  6658  nnmcan  6665  isotilem  7173  eqinfti  7187  inflbti  7191  infglbti  7192  djuf1olem  7220  dfmpq2  7542  axsuploc  8219  div4p1lem1div2  9365  ztri3or  9489  nn0ind-raph  9564  zindd  9565  qreccl  9837  elpq  9844  iooshf  10148  fzofzim  10388  elfzomelpfzo  10437  zmodid2  10574  q2submod  10607  modfzo0difsn  10617  frec2uzltd  10625  frec2uzled  10651  prhash2ex  11031  swrd0g  11192  pfxn0  11220  swrdswrd  11237  pfxccat3  11266  iserex  11850  prodrbdc  12085  reef11  12210  absdvdsb  12320  dvdsabsb  12321  modmulconst  12334  dvdsadd  12347  dvdsabseq  12358  odd2np1  12384  mod2eq0even  12389  oddnn02np1  12391  oddge22np1  12392  evennn02n  12393  evennn2n  12394  zeo5  12399  gcdass  12536  lcmdvds  12601  lcmass  12607  divgcdcoprm0  12623  divgcdcoprmex  12624  1nprm  12636  dvdsnprmd  12647  isevengcd2  12680  m1dvdsndvds  12771  sgrppropd  13446  issubm2  13506  rngpropd  13918  rhmf1o  14132  isrim  14133  2lgslem1a  15767  edg0iedg0g  15866  uhgreq12g  15876  uhgrvtxedgiedgb  15941