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 ) )

This proof depends on syntax axioms:   -> wi 4   <-> wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  impbid2  143  imbitrrid  156  ibir  177  bitr2d  189  bitr3d  190  bitr4d  191  bitr2id  193  bitr2di  197  pm5.5  242  anabs5  579  annotanannot  680  con2bidc  887  con1biidc  889  con2biidc  891  pm4.63dc  898  pm4.64dc  912  pm5.55dc  925  baibr  932  baibd  935  rbaibd  936  pm5.75  975  ninba  985  xor3dc  1436  3impexpbicomi  1489  cbvexv1  1805  cbvexh  1808  sbequ12r  1825  sbco  2028  sbcomxyyz  2032  sbal1yz  2061  cbvab  2364  eqabcdv  2370  nnedc  2425  necon3bbid  2460  necon2abiidc  2484  necon2bbiidc  2485  sbralie  2804  gencbvex  2869  gencbval  2871  sbhypf  2872  clel3g  2960  reu8  3022  sbceq2a  3062  sbcco2  3074  reu8nf  3133  sbcsng  3768  ssdifsn  3842  opabid  4400  soeq2  4463  tfisi  4736  posng  4849  xpiindim  4919  fvopab6  5808  fconstfvm  5936  cbvfo  5994  cbvexfo  5995  f1eqcocnv  6000  isoid  6019  isoini  6027  riotaeqimp  6066  resoprab2  6188  dfoprab3  6429  cnvoprab  6474  nnacan  6789  nnmcan  6796  mapsnd  6974  funisfsupp  7296  suppeqfsuppbi  7300  isotilem  7352  eqinfti  7366  inflbti  7370  infglbti  7371  djuf1olem  7399  dfmpq2  7728  axsuploc  8404  div4p1lem1div2  9570  ztri3or  9698  nn0ind-raph  9774  zindd  9775  qreccl  10058  elpq  10066  iooshf  10371  fzofzim  10617  elfzomelpfzo  10666  zmodid2  10810  q2submod  10843  modfzo0difsn  10853  frec2uzltd  10861  frec2uzled  10887  prhash2ex  11272  hashf1lem2  11308  swrd0g  11454  pfxn0  11482  swrdswrd  11499  pfxccat3  11528  iserex  12130  prodrbdc  12366  reef11  12491  absdvdsb  12601  dvdsabsb  12602  modmulconst  12615  dvdsadd  12628  dvdsabseq  12639  odd2np1  12665  mod2eq0even  12670  oddnn02np1  12672  oddge22np1  12673  evennn02n  12674  evennn2n  12675  zeo5  12680  gcdass  12817  lcmdvds  12882  lcmass  12888  divgcdcoprm0  12904  divgcdcoprmex  12905  1nprm  12917  dvdsnprmd  12928  isevengcd2  12962  m1dvdsndvds  13056  sgrppropd  13787  issubm2  13839  sscntz  14158  rngpropd  14361  rhmf1o  14584  isrim  14585  2lgslem1a  16412  edg0iedg0g  16512  uhgreq12g  16522  uhgrvtxedgiedgb  16589  edg0usgr  16693  umgrclwwlkge2  16848  isclwwlknx  16862  clwwlknonel  16878  clwwlknun  16887  ralrals  17356  rexrals  17357  ralals  17362  rexals  17363