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  4398  soeq2  4461  tfisi  4734  posng  4847  xpiindim  4917  fvopab6  5805  fconstfvm  5933  cbvfo  5991  cbvexfo  5992  f1eqcocnv  5997  isoid  6016  isoini  6024  riotaeqimp  6063  resoprab2  6185  dfoprab3  6425  cnvoprab  6470  nnacan  6785  nnmcan  6792  mapsnd  6970  funisfsupp  7291  suppeqfsuppbi  7295  isotilem  7347  eqinfti  7361  inflbti  7365  infglbti  7366  djuf1olem  7394  dfmpq2  7723  axsuploc  8399  div4p1lem1div2  9564  ztri3or  9692  nn0ind-raph  9768  zindd  9769  qreccl  10052  elpq  10060  iooshf  10365  fzofzim  10611  elfzomelpfzo  10660  zmodid2  10804  q2submod  10837  modfzo0difsn  10847  frec2uzltd  10855  frec2uzled  10881  prhash2ex  11266  hashf1lem2  11302  swrd0g  11448  pfxn0  11476  swrdswrd  11493  pfxccat3  11522  iserex  12124  prodrbdc  12360  reef11  12485  absdvdsb  12595  dvdsabsb  12596  modmulconst  12609  dvdsadd  12622  dvdsabseq  12633  odd2np1  12659  mod2eq0even  12664  oddnn02np1  12666  oddge22np1  12667  evennn02n  12668  evennn2n  12669  zeo5  12674  gcdass  12811  lcmdvds  12876  lcmass  12882  divgcdcoprm0  12898  divgcdcoprmex  12899  1nprm  12911  dvdsnprmd  12922  isevengcd2  12956  m1dvdsndvds  13050  sgrppropd  13781  issubm2  13833  sscntz  14152  rngpropd  14338  rhmf1o  14559  isrim  14560  2lgslem1a  16373  edg0iedg0g  16473  uhgreq12g  16483  uhgrvtxedgiedgb  16550  edg0usgr  16654  umgrclwwlkge2  16809  isclwwlknx  16823  clwwlknonel  16839  clwwlknun  16848  ralrals  17316  rexrals  17317  ralals  17322  rexals  17323