MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  bicomi Unicode version

Theorem bicomi 193
Description: Inference from commutative law for logical equivalence. (Contributed by NM, 5-Aug-1993.)
Hypothesis
Ref Expression
bicomi.1  |-  ( ph  <->  ps )
Assertion
Ref Expression
bicomi  |-  ( ps  <->  ph )

Proof of Theorem bicomi
StepHypRef Expression
1 bicomi.1 . 2  |-  ( ph  <->  ps )
2 bicom1 190 . 2  |-  ( (
ph 
<->  ps )  ->  ( ps 
<-> 
ph ) )
31, 2ax-mp 8 1  |-  ( ps  <->  ph )
Colors of variables: wff set class
Syntax hints:    <-> wb 176
This theorem is referenced by:  biimpri  197  bitr2i  241  bitr3i  242  bitr4i  243  syl5bbr  250  syl5rbbr  251  syl6bbr  254  syl6rbbr  255  mtbir  290  sylnibr  296  sylnbir  298  xchnxbir  300  xchbinxr  302  con1bii  321  con2bii  322  nbn  336  xor3  346  pm5.41  353  pm4.64  361  pm4.63  410  pm4.61  415  anor  475  pm4.53  478  pm4.55  480  pm4.56  481  pm4.57  483  pm4.25  501  pm4.87  567  anidm  625  pm4.77  762  anabs1  783  anabs7  785  pm4.76  836  pm5.63  890  3ianor  949  3oran  951  pm3.2an3  1131  syl3anbr  1226  3an6  1262  nannot  1293  truimfal  1335  nottru  1338  nic-dfim  1424  nic-dfneg  1425  2nalexn  1560  sbid  1863  dvelimf  1937  cleljust  1954  cleljustALT  1955  sb10f  2061  nne  2450  necon3bbii  2477  necon2abii  2501  necon2bbii  2502  alexeq  2897  ceqsrexbv  2902  clel2  2904  clel4  2907  2reu5lem1  2970  2reu5lem2  2971  2reu5lem3  2972  dfsbcq2  2994  cbvreucsf  3145  nss  3236  difab  3437  un0  3479  in0  3480  ss0b  3484  ssunsn2  3773  iindif2  3971  nssss  4229  epse  4376  uniuni  4527  reusv2lem4  4538  cotr  5055  issref  5056  mptpreima  5166  ralrnmpt  5669  weniso  5852  eroveu  6753  isfinite2  7115  marypha1lem  7186  marypha2lem4  7191  en3lplem2  7417  carden2  7620  fseqenlem1  7651  iscard3  7720  cardnum  7721  alephinit  7722  cardinfima  7724  alephiso  7725  dfac10b  7765  dfackm  7792  isfin5-2  8017  brdom7disj  8156  brdom6disj  8157  splfv1  11470  vdwapun  13021  grpss  14503  drngnidl  15981  drnglpir  16005  unocv  16580  toptopon  16671  ordtbas2  16921  ordtrest2  16934  xmeterval  17978  ovolfcl  18826  eldv  19248  eltayl  19739  musumsum  20432  lejdii  22117  mdslle1i  22897  mdslle2i  22898  mdslj1i  22899  mdslj2i  22900  ballotlem2  23047  mo5f  23143  disjex  23176  unipreima  23209  relexpindlem  24036  cnvco1  24117  cnvco2  24118  elfuns  24454  dfiota3  24462  funpartfv  24483  nabi1i  24830  nabi2i  24831  negcmpprcal2  24946  eqvinopb  24965  boxeq  24987  notev  24990  notal  24991  albineal  24999  splint  25048  restidsing  25076  imfstnrelc  25081  defse3  25272  qusp  25542  algi  25727  prismorcsetlemc  25917  nbssntrs  26147  trer  26227  inixp  26399  an43  26712  rmxypairf1o  26996  dsmmacl  27207  pmtrfrn  27400  acsfn1p  27507  pm10.252  27556  pm10.253  27557  pm10.42  27559  2nexaln  27573  aaanv  27587  pm13.195  27613  pm13.196a  27614  rfcnnnub  27707  aovov0bi  28056  f1oun2prg  28076  s4f1o  28093  nbgranself2  28151  frgra3v  28180  sbc3org  28295  en3lpVD  28621  3orbi123VD  28626  sbc3orgVD  28627  undif3VD  28658  a9e2ndeqVD  28685  a9e2ndeqALT  28708  bnj115  28751  bnj156  28756  bnj206  28759  bnj110  28890  bnj121  28902  bnj124  28903  bnj130  28906  bnj153  28912  bnj207  28913  bnj605  28939  bnj581  28940  bnj611  28950  bnj864  28954  bnj865  28955  bnj893  28960  bnj1000  28973  bnj978  28981  bnj1040  29002  bnj1049  29004  bnj1133  29019  bnj1189  29039  isopos  29370  islvol5  29768  elpadd0  29998  dvhopellsm  31307  diblsmopel  31361  mapdvalc  31819
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177
  Copyright terms: Public domain W3C validator