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

Theorem bicomd 139
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 138 . 2  |-  ( ( ps  <->  ch )  <->  ( ch  <->  ps ) )
31, 2sylib 120 1  |-  ( ph  ->  ( ch  <->  ps )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 103
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106
This theorem depends on definitions:  df-bi 115
This theorem is referenced by:  impbid2  141  syl5ibr  154  ibir  175  bitr2d  187  bitr3d  188  bitr4d  189  syl5rbb  191  syl6rbb  195  pm5.5  240  anabs5  538  con2bidc  803  con1biidc  805  con2biidc  807  pm4.63dc  814  pm4.64dc  835  pm5.55dc  853  baibr  863  baibd  866  rbaibd  867  pm4.55dc  880  anordc  898  pm5.75  904  ninba  914  xor3dc  1319  3impexpbicomi  1369  cbvexh  1679  sbequ12r  1696  sbco  1884  sbcomxyyz  1888  sbal1yz  1919  cbvab  2202  nnedc  2251  necon3bbid  2286  necon2abiidc  2310  necon2bbii  2311  gencbvex  2646  gencbval  2648  sbhypf  2649  clel3g  2730  reu8  2789  sbceq2a  2826  sbcco2  2838  sbcsng  3459  opabid  4020  soeq2  4079  tfisi  4336  posng  4438  xpiindim  4501  fvopab6  5296  fconstfvm  5411  cbvfo  5456  cbvexfo  5457  f1eqcocnv  5462  isoid  5481  isoini  5488  resoprab2  5629  dfoprab3  5848  cnvoprab  5886  nnacan  6151  nnmcan  6158  isotilem  6478  eqinfti  6492  inflbti  6496  infglbti  6497  dfmpq2  6607  div4p1lem1div2  8351  ztri3or  8475  nn0ind-raph  8545  zindd  8546  qreccl  8808  iooshf  9051  fzofzim  9274  elfzomelpfzo  9317  zmodid2  9434  q2submod  9467  modfzo0difsn  9477  frec2uzltd  9485  frec2uzled  9511  prsize2ex  9833  iiserex  10315  absdvdsb  10358  dvdsabsb  10359  modmulconst  10372  dvdsadd  10383  dvdsabseq  10392  odd2np1  10417  mod2eq0even  10422  oddnn02np1  10424  oddge22np1  10425  evennn02n  10426  evennn2n  10427  zeo5  10432  gcdass  10548  lcmdvds  10605  lcmass  10611  divgcdcoprm0  10627  divgcdcoprmex  10628  1nprm  10640  dvdsnprmd  10651  isevengcd2  10681  bj-indeq  10882
  Copyright terms: Public domain W3C validator