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  7346  eqinfti  7360  inflbti  7364  infglbti  7365  djuf1olem  7393  dfmpq2  7722  axsuploc  8398  div4p1lem1div2  9559  ztri3or  9687  nn0ind-raph  9763  zindd  9764  qreccl  10042  elpq  10049  iooshf  10354  fzofzim  10600  elfzomelpfzo  10649  zmodid2  10789  q2submod  10822  modfzo0difsn  10832  frec2uzltd  10840  frec2uzled  10866  prhash2ex  11250  hashf1lem2  11286  swrd0g  11432  pfxn0  11460  swrdswrd  11477  pfxccat3  11506  iserex  12105  prodrbdc  12341  reef11  12466  absdvdsb  12576  dvdsabsb  12577  modmulconst  12590  dvdsadd  12603  dvdsabseq  12614  odd2np1  12640  mod2eq0even  12645  oddnn02np1  12647  oddge22np1  12648  evennn02n  12649  evennn2n  12650  zeo5  12655  gcdass  12792  lcmdvds  12857  lcmass  12863  divgcdcoprm0  12879  divgcdcoprmex  12880  1nprm  12892  dvdsnprmd  12903  isevengcd2  12936  m1dvdsndvds  13027  sgrppropd  13728  issubm2  13780  rngpropd  14254  rhmf1o  14475  isrim  14476  2lgslem1a  16207  edg0iedg0g  16307  uhgreq12g  16317  uhgrvtxedgiedgb  16384  edg0usgr  16488  umgrclwwlkge2  16643  isclwwlknx  16657  clwwlknonel  16673  clwwlknun  16682  ralrals  17149  rexrals  17150  ralals  17155  rexals  17156