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

Theorem bicomi 202
Description: Inference from commutative law for logical equivalence. (Contributed by NM, 3-Jan-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 199 . 2  |-  ( (
ph 
<->  ps )  ->  ( ps 
<-> 
ph ) )
31, 2ax-mp 5 1  |-  ( ps  <->  ph )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 184
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 185
This theorem is referenced by:  biimpri  206  bitr2i  250  bitr3i  251  bitr4i  252  syl5bbr  259  syl5rbbr  260  syl6bbr  263  syl6rbbr  264  mtbir  299  sylnibr  305  sylnbir  307  xchnxbir  309  xchbinxr  311  con1bii  331  con2bii  332  nbn  347  xor3  357  pm5.41  364  pm4.64  372  pm4.63  421  pm4.61  426  anor  489  pm4.53  492  pm4.55  494  pm4.56  495  pm4.57  497  pm4.25  515  pm4.87  584  anidm  644  pm4.77  785  anabs1  806  anabs7  808  pm4.76  861  pm5.63  915  jaoi2OLD  960  3ianor  982  3oran  984  pm3.2an3  1167  syl3anbr  1262  3an6  1299  nannot  1339  truan  1386  truimfal  1402  nottru  1405  nic-dfim  1476  nic-dfneg  1477  2nalexn  1619  2nexaln  1621  sbequ8  1705  dvelimf  2026  cleljust  2059  cleljustALT  2060  sb5rf  2120  sb6rf  2122  sb10f  2166  nne  2607  necon3bbii  2634  necon2abii  2661  necon2bbii  2662  nabbi  2701  nnel  2709  alexeq  3084  ceqsrexbv  3089  clel2  3091  clel4  3094  2reu5lem1  3159  2reu5lem2  3160  2reu5lem3  3161  dfsbcq2  3184  cbvreucsf  3316  nss  3409  raldifb  3491  difab  3614  un0  3657  in0  3658  ss0b  3662  ssunsn2  4027  iindif2  4234  nssss  4543  opthneg  4566  epse  4698  restidsing  5157  cotr  5205  issref  5206  mptpreima  5326  ralrnmpt  5847  fmptsng  5895  weniso  6040  uniuni  6380  suppvalbr  6689  eroveu  7187  isfinite2  7562  marypha1lem  7675  marypha2lem4  7680  wemapso2lem  7759  en3lplem2  7813  cantnfp1  7881  carden2  8149  fseqenlem1  8186  iscard3  8255  cardnum  8256  alephinit  8257  cardinfima  8259  alephiso  8260  dfac10b  8300  dfackm  8327  isfin5-2  8552  brdom7disj  8690  brdom6disj  8691  hashtpg  12178  wrdeqswrdlsw  12335  wrd2ind  12364  splfv1  12389  cshwsexa  12450  s4f1o  12520  vdwapun  14027  cshwsiun  14118  cshwshash  14123  grpss  15550  pmtrfrn  15955  pmtrrn2  15957  pmtrprfvalrn  15985  issrg  16597  drngnidl  17288  drnglpir  17312  unocv  18080  dsmmacl  18141  toptopon  18513  ordtbas2  18770  ordtrest2  18783  restutopopn  19788  xmeterval  19982  ovolfcl  20925  eldv  21348  eltayl  21800  musumsum  22507  usgrafilem1  23275  trls  23386  is2wlk  23415  lejdii  24892  mdslle1i  25672  mdslle2i  25673  mdslj1i  25674  mdslj2i  25675  spc2ed  25808  mo5f  25819  unipreima  25912  2ndpreima  25953  xrge0infss  26004  ordtrest2NEW  26305  ordtconlem1  26306  ballotlem2  26823  plymulx0  26900  relexpindlem  27292  fprod2dlem  27442  cnvco1  27521  cnvco2  27522  dfiota3  27905  nabi1i  28189  nabi2i  28190  wl-sb8eut  28351  trer  28464  inixp  28575  notbinot1  28832  impor  28834  notbinot2  28836  truconj  28857  sbcalf  28873  sbcexf  28874  exlimddvfi  28883  sbccom2lem  28886  sbccom2  28887  sbccom2f  28888  tsim1  28894  tsxo3  28903  tsxo4  28904  an43  28946  rmxypairf1o  29205  acsfn1p  29509  pm10.252  29566  pm10.253  29567  pm10.42  29569  aaanv  29594  pm13.195  29620  pm13.196a  29621  aibandbiaiffaiffb  29861  aovov0bi  30055  rexdifpr  30077  dff14a  30097  f13dfv  30100  rabasiun  30183  wwlknndef  30322  wlknwwlknvbij  30325  el2wlkonotot0  30344  usg2spthonot0  30361  clwwlknndef  30389  clwwlkvbij  30416  frgraun  30541  frgra2v  30544  4cycl2vnunb  30562  vdn0frgrav2  30569  vdgn0frgrav2  30570  2spotdisj  30607  usg2spot2nb  30611  usgreg2spot  30613  frgraregord013  30664  fmptsnd  30674  pgrpgt2nabel  30720  0rngnnzr  30729  fsuppmapnn0fiubex  30749  pmatcollpw2lem  30820  lindslinindsimp2lem5  30885  islininds2  30907  ldepslinc  30940  sbc3or  31124  sbc3orgOLD  31125  en3lpVD  31468  3orbi123VD  31473  sbc3orgVD  31474  undif3VD  31505  ax6e2ndeqVD  31532  ax6e2ndeqALT  31554  sineq0ALT  31560  bnj115  31601  bnj156  31606  bnj206  31609  bnj110  31738  bnj121  31750  bnj124  31751  bnj130  31754  bnj153  31760  bnj207  31761  bnj581  31788  bnj611  31798  bnj864  31802  bnj865  31803  bnj893  31808  bnj1000  31821  bnj978  31829  bnj1040  31850  bnj1049  31852  bnj1133  31867  bnj1189  31887  bj-dfifc2  31986  bj-df-ifc  31987  bj-nf3  32013  bj-nfdt  32058  bj-cleljust  32136  bj-denotes  32218  bj-ralcom4  32228  bj-rexcom4  32229  bj-elsngl  32308  isopos  32665  islvol5  33063  elpadd0  33293  dvhopellsm  34602  diblsmopel  34656  mapdvalc  35114
  Copyright terms: Public domain W3C validator