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  575  annotanannot  676  con2bidc  883  con1biidc  885  con2biidc  887  pm4.63dc  894  pm4.64dc  908  pm5.55dc  921  baibr  928  baibd  931  rbaibd  932  pm5.75  971  ninba  981  xor3dc  1432  3impexpbicomi  1485  cbvexv1  1801  cbvexh  1804  sbequ12r  1821  sbco  2024  sbcomxyyz  2028  sbal1yz  2057  cbvab  2360  eqabcdv  2366  nnedc  2419  necon3bbid  2454  necon2abiidc  2478  necon2bbiidc  2479  sbralie  2798  gencbvex  2863  gencbval  2865  sbhypf  2866  clel3g  2953  reu8  3015  sbceq2a  3055  sbcco2  3067  reu8nf  3126  sbcsng  3750  ssdifsn  3823  opabid  4376  soeq2  4439  tfisi  4711  posng  4824  xpiindim  4894  fvopab6  5776  fconstfvm  5904  cbvfo  5960  cbvexfo  5961  f1eqcocnv  5966  isoid  5985  isoini  5993  riotaeqimp  6030  resoprab2  6152  dfoprab3  6387  cnvoprab  6432  nnacan  6747  nnmcan  6754  mapsnd  6925  funisfsupp  7246  suppeqfsuppbi  7250  isotilem  7299  eqinfti  7313  inflbti  7317  infglbti  7318  djuf1olem  7346  dfmpq2  7672  axsuploc  8348  div4p1lem1div2  9494  ztri3or  9622  nn0ind-raph  9698  zindd  9699  qreccl  9977  elpq  9984  iooshf  10288  fzofzim  10531  elfzomelpfzo  10580  zmodid2  10718  q2submod  10751  modfzo0difsn  10761  frec2uzltd  10769  frec2uzled  10795  prhash2ex  11178  swrd0g  11356  pfxn0  11384  swrdswrd  11401  pfxccat3  11430  iserex  12028  prodrbdc  12264  reef11  12389  absdvdsb  12499  dvdsabsb  12500  modmulconst  12513  dvdsadd  12526  dvdsabseq  12537  odd2np1  12563  mod2eq0even  12568  oddnn02np1  12570  oddge22np1  12571  evennn02n  12572  evennn2n  12573  zeo5  12578  gcdass  12715  lcmdvds  12780  lcmass  12786  divgcdcoprm0  12802  divgcdcoprmex  12803  1nprm  12815  dvdsnprmd  12826  isevengcd2  12859  m1dvdsndvds  12950  sgrppropd  13643  issubm2  13703  rngpropd  14116  rhmf1o  14330  isrim  14331  2lgslem1a  15978  edg0iedg0g  16078  uhgreq12g  16088  uhgrvtxedgiedgb  16155  edg0usgr  16259  umgrclwwlkge2  16414  isclwwlknx  16428  clwwlknonel  16444  clwwlknun  16453