ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  bicomd Unicode version

Theorem bicomd 129
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
StepHypRef Expression
1 bicomd.1 . 2  |-  ( ph  ->  ( ps  <->  ch )
)
2 bicom 128 . 2  |-  ( ( ps  <->  ch )  <->  ( ch  <->  ps ) )
31, 2sylib 127 1  |-  ( ph  ->  ( ch  <->  ps )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 98
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101
This theorem depends on definitions:  df-bi 110
This theorem is referenced by:  impbid2  131  syl5ibr  145  ibir  166  bitr2d  178  bitr3d  179  bitr4d  180  syl5rbb  182  syl6rbb  186  pm5.5  231  anabs5  507  con2bidc  769  con1biidc  771  con2biidc  773  pm4.63dc  780  pm4.64dc  801  pm5.55dc  819  baibr  829  baibd  832  rbaibd  833  pm4.55dc  846  anordc  863  pm5.75  869  ninba  879  xor3dc  1278  3impexpbicomi  1328  cbvexh  1638  sbequ12r  1655  sbco  1842  sbcomxyyz  1846  sbal1yz  1877  cbvab  2160  nnedc  2211  necon3bbid  2245  necon2abiidc  2269  necon2bbii  2270  gencbvex  2600  gencbval  2602  sbhypf  2603  clel3g  2678  reu8  2737  sbceq2a  2774  sbcco2  2786  sbcsng  3429  opabid  3994  soeq2  4053  tfisi  4310  posng  4412  xpiindim  4473  fvopab6  5264  fconstfvm  5379  cbvfo  5425  cbvexfo  5426  f1eqcocnv  5431  isoid  5450  isoini  5457  resoprab2  5598  dfoprab3  5817  nnacan  6085  nnmcan  6092  dfmpq2  6453  div4p1lem1div2  8177  ztri3or  8288  nn0ind-raph  8355  zindd  8356  qreccl  8576  iooshf  8821  fzofzim  9044  elfzomelpfzo  9087  frec2uzltd  9189  iiserex  9859  bj-indeq  10053
  Copyright terms: Public domain W3C validator