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  5733  fconstfvm  5861  cbvfo  5915  cbvexfo  5916  f1eqcocnv  5921  isoid  5940  isoini  5948  riotaeqimp  5985  resoprab2  6107  dfoprab3  6343  cnvoprab  6386  nnacan  6666  nnmcan  6673  isotilem  7184  eqinfti  7198  inflbti  7202  infglbti  7203  djuf1olem  7231  dfmpq2  7553  axsuploc  8230  div4p1lem1div2  9376  ztri3or  9500  nn0ind-raph  9575  zindd  9576  qreccl  9849  elpq  9856  iooshf  10160  fzofzim  10400  elfzomelpfzo  10449  zmodid2  10586  q2submod  10619  modfzo0difsn  10629  frec2uzltd  10637  frec2uzled  10663  prhash2ex  11044  swrd0g  11208  pfxn0  11236  swrdswrd  11253  pfxccat3  11282  iserex  11866  prodrbdc  12101  reef11  12226  absdvdsb  12336  dvdsabsb  12337  modmulconst  12350  dvdsadd  12363  dvdsabseq  12374  odd2np1  12400  mod2eq0even  12405  oddnn02np1  12407  oddge22np1  12408  evennn02n  12409  evennn2n  12410  zeo5  12415  gcdass  12552  lcmdvds  12617  lcmass  12623  divgcdcoprm0  12639  divgcdcoprmex  12640  1nprm  12652  dvdsnprmd  12663  isevengcd2  12696  m1dvdsndvds  12787  sgrppropd  13462  issubm2  13522  rngpropd  13934  rhmf1o  14148  isrim  14149  2lgslem1a  15783  edg0iedg0g  15882  uhgreq12g  15892  uhgrvtxedgiedgb  15957  umgrclwwlkge2  16145  isclwwlknx  16158