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  877  con1biidc  879  con2biidc  881  pm4.63dc  888  pm4.64dc  902  pm5.55dc  915  baibr  922  baibd  925  rbaibd  926  pm5.75  965  ninba  975  xor3dc  1407  3impexpbicomi  1459  cbvexv1  1775  cbvexh  1778  sbequ12r  1795  sbco  1996  sbcomxyyz  2000  sbal1yz  2029  cbvab  2329  nnedc  2381  necon3bbid  2416  necon2abiidc  2440  necon2bbiidc  2441  sbralie  2756  gencbvex  2819  gencbval  2821  sbhypf  2822  clel3g  2907  reu8  2969  sbceq2a  3009  sbcco2  3021  sbcsng  3692  ssdifsn  3761  opabid  4303  soeq2  4364  tfisi  4636  posng  4748  xpiindim  4816  fvopab6  5678  fconstfvm  5804  cbvfo  5856  cbvexfo  5857  f1eqcocnv  5862  isoid  5881  isoini  5889  resoprab2  6044  dfoprab3  6279  cnvoprab  6322  nnacan  6600  nnmcan  6607  isotilem  7110  eqinfti  7124  inflbti  7128  infglbti  7129  djuf1olem  7157  dfmpq2  7470  axsuploc  8147  div4p1lem1div2  9293  ztri3or  9417  nn0ind-raph  9492  zindd  9493  qreccl  9765  elpq  9772  iooshf  10076  fzofzim  10314  elfzomelpfzo  10362  zmodid2  10499  q2submod  10532  modfzo0difsn  10542  frec2uzltd  10550  frec2uzled  10576  prhash2ex  10956  swrd0g  11116  pfxn0  11142  iserex  11683  prodrbdc  11918  reef11  12043  absdvdsb  12153  dvdsabsb  12154  modmulconst  12167  dvdsadd  12180  dvdsabseq  12191  odd2np1  12217  mod2eq0even  12222  oddnn02np1  12224  oddge22np1  12225  evennn02n  12226  evennn2n  12227  zeo5  12232  gcdass  12369  lcmdvds  12434  lcmass  12440  divgcdcoprm0  12456  divgcdcoprmex  12457  1nprm  12469  dvdsnprmd  12480  isevengcd2  12513  m1dvdsndvds  12604  sgrppropd  13278  issubm2  13338  rngpropd  13750  rhmf1o  13963  isrim  13964  2lgslem1a  15598  edg0iedg0g  15693