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  805  con1biidc  807  con2biidc  809  pm4.63dc  816  pm4.64dc  837  pm5.55dc  855  baibr  865  baibd  868  rbaibd  869  pm4.55dc  882  anordc  900  pm5.75  906  ninba  916  xor3dc  1321  3impexpbicomi  1371  cbvexh  1682  sbequ12r  1699  sbco  1887  sbcomxyyz  1891  sbal1yz  1922  cbvab  2207  nnedc  2256  necon3bbid  2291  necon2abiidc  2315  necon2bbii  2316  gencbvex  2659  gencbval  2661  sbhypf  2662  clel3g  2742  reu8  2802  sbceq2a  2839  sbcco2  2851  sbcsng  3484  ssdifsn  3551  opabid  4057  soeq2  4116  tfisi  4374  posng  4477  xpiindim  4540  fvopab6  5353  fconstfvm  5470  cbvfo  5519  cbvexfo  5520  f1eqcocnv  5525  isoid  5544  isoini  5552  resoprab2  5693  dfoprab3  5912  cnvoprab  5950  nnacan  6217  nnmcan  6224  isotilem  6638  eqinfti  6652  inflbti  6656  infglbti  6657  djuf1olem  6682  dfmpq2  6851  div4p1lem1div2  8595  ztri3or  8719  nn0ind-raph  8789  zindd  8790  qreccl  9052  iooshf  9295  fzofzim  9520  elfzomelpfzo  9563  zmodid2  9680  q2submod  9713  modfzo0difsn  9723  frec2uzltd  9731  frec2uzled  9757  prhash2ex  10106  iiserex  10612  absdvdsb  10681  dvdsabsb  10682  modmulconst  10695  dvdsadd  10706  dvdsabseq  10715  odd2np1  10740  mod2eq0even  10745  oddnn02np1  10747  oddge22np1  10748  evennn02n  10749  evennn2n  10750  zeo5  10755  gcdass  10871  lcmdvds  10928  lcmass  10934  divgcdcoprm0  10950  divgcdcoprmex  10951  1nprm  10963  dvdsnprmd  10974  isevengcd2  11004  bj-indeq  11254
  Copyright terms: Public domain W3C validator