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-mp 5  ax-1 6  ax-2 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  bitr2id  192  bitr2di  196  pm5.5  241  anabs5  568  con2bidc  870  con1biidc  872  con2biidc  874  pm4.63dc  881  pm4.64dc  895  pm5.55dc  908  baibr  915  baibd  918  rbaibd  919  pm4.55dc  933  anordc  951  pm5.75  957  ninba  967  xor3dc  1382  3impexpbicomi  1432  cbvexv1  1745  cbvexh  1748  sbequ12r  1765  sbco  1961  sbcomxyyz  1965  sbal1yz  1994  cbvab  2294  nnedc  2345  necon3bbid  2380  necon2abiidc  2404  necon2bbiidc  2405  sbralie  2714  gencbvex  2776  gencbval  2778  sbhypf  2779  clel3g  2864  reu8  2926  sbceq2a  2965  sbcco2  2977  sbcsng  3642  ssdifsn  3711  opabid  4242  soeq2  4301  tfisi  4571  posng  4683  xpiindim  4748  fvopab6  5592  fconstfvm  5714  cbvfo  5764  cbvexfo  5765  f1eqcocnv  5770  isoid  5789  isoini  5797  resoprab2  5950  dfoprab3  6170  cnvoprab  6213  nnacan  6491  nnmcan  6498  isotilem  6983  eqinfti  6997  inflbti  7001  infglbti  7002  djuf1olem  7030  dfmpq2  7317  axsuploc  7992  div4p1lem1div2  9131  ztri3or  9255  nn0ind-raph  9329  zindd  9330  qreccl  9601  elpq  9607  iooshf  9909  fzofzim  10144  elfzomelpfzo  10187  zmodid2  10308  q2submod  10341  modfzo0difsn  10351  frec2uzltd  10359  frec2uzled  10385  prhash2ex  10744  iserex  11302  prodrbdc  11537  reef11  11662  absdvdsb  11771  dvdsabsb  11772  modmulconst  11785  dvdsadd  11798  dvdsabseq  11807  odd2np1  11832  mod2eq0even  11837  oddnn02np1  11839  oddge22np1  11840  evennn02n  11841  evennn2n  11842  zeo5  11847  gcdass  11970  lcmdvds  12033  lcmass  12039  divgcdcoprm0  12055  divgcdcoprmex  12056  1nprm  12068  dvdsnprmd  12079  isevengcd2  12112  m1dvdsndvds  12202