Theorem bicomd 140

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 139	. 2 |- ( ( ps <-> ch ) <-> ( ch <-> ps ) )
3	1, 2	sylib 121	1 |- ( ph -> ( ch <-> ps ) )

Syntax hints:   -> wi 4   <-> wb 104

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  impbid2  142  syl5ibr  155  ibir  176  bitr2d  188  bitr3d  189  bitr4d  190  syl5rbb  192  syl6rbb  196  pm5.5  241  anabs5  545  con2bidc  841  con1biidc  843  con2biidc  845  pm4.63dc  852  pm4.64dc  866  pm5.55dc  879  baibr  886  baibd  889  rbaibd  890  pm4.55dc  903  anordc  921  pm5.75  927  ninba  937  xor3dc  1346  3impexpbicomi  1396  cbvexh  1709  sbequ12r  1726  sbco  1915  sbcomxyyz  1919  sbal1yz  1950  cbvab  2235  nnedc  2285  necon3bbid  2320  necon2abiidc  2344  necon2bbiidc  2345  sbralie  2639  gencbvex  2701  gencbval  2703  sbhypf  2704  clel3g  2787  reu8  2847  sbceq2a  2886  sbcco2  2898  sbcsng  3546  ssdifsn  3615  opabid  4137  soeq2  4196  tfisi  4459  posng  4569  xpiindim  4634  fvopab6  5469  fconstfvm  5590  cbvfo  5638  cbvexfo  5639  f1eqcocnv  5644  isoid  5663  isoini  5671  resoprab2  5820  dfoprab3  6041  cnvoprab  6083  nnacan  6360  nnmcan  6367  isotilem  6843  eqinfti  6857  inflbti  6861  infglbti  6862  djuf1olem  6888  dfmpq2  7105  div4p1lem1div2  8871  ztri3or  8995  nn0ind-raph  9066  zindd  9067  qreccl  9330  iooshf  9622  fzofzim  9852  elfzomelpfzo  9895  zmodid2  10012  q2submod  10045  modfzo0difsn  10055  frec2uzltd  10063  frec2uzled  10089  prhash2ex  10442  iserex  10994  reef11  11251  absdvdsb  11353  dvdsabsb  11354  modmulconst  11367  dvdsadd  11378  dvdsabseq  11387  odd2np1  11412  mod2eq0even  11417  oddnn02np1  11419  oddge22np1  11420  evennn02n  11421  evennn2n  11422  zeo5  11427  gcdass  11543  lcmdvds  11600  lcmass  11606  divgcdcoprm0  11622  divgcdcoprmex  11623  1nprm  11635  dvdsnprmd  11646  isevengcd2  11676  bj-indeq  12810