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

Theorem bicomi 207
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 204 . 2  |-  ( (
ph 
<->  ps )  ->  ( ps 
<-> 
ph ) )
31, 2ax-mp 5 1  |-  ( ps  <->  ph )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 189
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 190
This theorem is referenced by:  biimpri  211  bitr2i  258  bitr3i  259  bitr4i  260  syl5bbr  267  syl5rbbr  268  syl6bbr  271  syl6rbbr  272  mtbir  305  sylnibr  311  sylnbir  313  xchnxbir  315  xchbinxr  317  con1bii  337  con2bii  338  nbn  353  xor3  363  pm5.41  370  pm4.64  378  pm4.63  427  pm4.61  432  anor  496  pm4.53  499  pm4.55  501  pm4.56  502  pm4.57  504  pm4.25  522  pm4.87  592  anidm  654  pm4.77  801  anabs1  822  anabs7  824  pm4.76  880  pm5.63  935  3ianor  1003  3oran  1005  pm3.2an3  1188  syl3anbr  1315  3an6  1353  nannot  1395  nanbi  1396  nanbiOLD  1397  truan  1465  truimfal  1479  nottru  1482  falbitru  1485  nic-dfim  1556  nic-dfneg  1557  2nalexn  1704  2nexaln  1706  sbequ8  1806  cleljust  1899  cleljustALT  2090  cleljustALT2  2091  dvelimf  2169  sb5rf  2252  sb6rf  2253  sb10f  2286  abeq1i  2565  nne  2628  necon3bbii  2671  necon2abii  2674  necon2bbii  2675  nnel  2733  ceqsrexbv  3141  clel2  3143  clel4  3146  2reu5lem1  3213  2reu5lem2  3214  2reu5lem3  3215  dfsbcq2  3238  cbvreucsf  3365  nss  3458  raldifb  3541  difab  3680  un0  3727  in0  3728  ss0b  3732  ssunsn2  4100  rabasiun  4252  iindif2  4317  nssss  4629  opthneg  4654  epse  4795  restidsing  5139  cotrg  5189  issref  5191  mptpreima  5307  ralrnmpt  6015  fmptsng  6070  fmptsnd  6071  dff14a  6156  f13dfv  6159  weniso  6231  fvmptopab2  6321  uniuni  6588  suppvalbr  6906  eroveu  7445  isfinite2  7816  marypha1lem  7934  marypha2lem4  7939  infcllem  7990  wemapso2lem  8054  en3lplem2  8107  cantnfp1  8173  carden2  8408  fseqenlem1  8442  iscard3  8511  cardnum  8512  alephinit  8513  cardinfima  8515  alephiso  8516  dfac10b  8556  dfackm  8583  isfin5-2  8808  brdom7disj  8946  brdom6disj  8947  fsuppmapnn0fiubex  12198  hash2prb  12628  hashtpg  12636  wrd2ind  12833  splfv1  12861  cshwsexa  12922  s4f1o  13011  cotr2g  13051  relexpindlem  13137  lcmfunsnlem2  14624  ncoprmlnprm  14688  vdwapun  14935  cshwsiun  15081  cshwshash  15086  grpss  16698  pmtrfrn  17110  pmtrrn2  17112  pmtrprfvalrn  17140  issrg  17752  drngnidl  18464  drnglpir  18488  0ringnnzr  18504  unocv  19254  dsmmacl  19315  pmatcollpw2lem  19812  fvmptnn04if  19884  toptopon  19959  ordtbas2  20218  ordtrest2  20231  xmeterval  21458  ovolfcl  22430  eldv  22865  eltayl  23327  musumsum  24133  usgrafilem1  25151  trls  25278  is2wlk  25307  wwlknndef  25477  wlknwwlknvbij  25480  clwwlknndef  25513  clwwlkvbij  25541  el2wlkonotot0  25612  usg2spthonot0  25629  frgraun  25736  frgra2v  25739  4cycl2vnunb  25757  vdn0frgrav2  25763  vdgn0frgrav2  25764  2spotdisj  25801  usg2spot2nb  25805  usgreg2spot  25807  frgraregord013  25858  lejdii  27203  mdslle1i  27982  mdslle2i  27983  mdslj1i  27984  mdslj2i  27985  mo5f  28132  unipreima  28254  2ndpreima  28296  xrge0infssOLD  28349  ordtrest2NEW  28736  ordtconlem1  28737  ballotlem2  29327  plymulx0  29442  bnj115  29537  bnj156  29542  bnj206  29545  bnj110  29675  bnj121  29687  bnj124  29688  bnj130  29691  bnj153  29697  bnj207  29698  bnj581  29725  bnj611  29735  bnj864  29739  bnj865  29740  bnj893  29745  bnj1000  29758  bnj978  29766  bnj1040  29787  bnj1049  29789  bnj1133  29804  bnj1189  29824  cnvco1  30406  cnvco2  30407  dfiota3  30696  trer  30978  nabi1i  31058  nabi2i  31059  bj-dfifc2  31160  bj-df-ifc  31161  bj-nf3  31195  bj-dfssb2  31255  bj-hbext  31306  bj-denotes  31469  bj-ralcom4  31479  bj-rexcom4  31480  bj-elsngl  31564  bj-nuliotaALT  31626  con1bii2  31736  con2bii2  31737  topdifinfeq  31755  isbasisrelowllem2  31761  wl-sb8eut  31908  inixp  32057  notbinot1  32314  notbinot2  32318  truconj  32339  sbccom2lem  32366  sbccom2  32367  sbccom2f  32368  tsim1  32374  tsxo3  32383  tsxo4  32384  an43  32425  isopos  32748  islvol5  33146  elpadd0  33376  dvhopellsm  34687  diblsmopel  34741  mapdvalc  35199  rmxypairf1o  35761  acsfn1p  36067  ifpnotnotb  36125  ifpdfxor  36133  ifpidg  36137  ifpim123g  36146  ifpim1g  36147  ifpimimb  36150  ifpimim  36155  rp-fakeanorass  36159  rp-isfinite6  36165  elmapintrab  36184  undmrnresiss  36212  clcnvlem  36232  cnviun  36244  dfxor4  36360  dfhe3  36372  dffrege69  36530  dffrege76  36537  pm10.252  36711  pm10.253  36712  pm10.42  36714  aaanv  36739  pm13.195  36765  pm13.196a  36766  sbc3or  36890  sbc3orgOLD  36894  en3lpVD  37238  3orbi123VD  37243  sbc3orgVD  37244  undif3VD  37276  ax6e2ndeqVD  37303  ax6e2ndeqALT  37325  sineq0ALT  37331  uzwo4  37387  inn0f  37412  rnmptpr  37454  fompt  37477  mapsnend  37490  cncfshift  37793  dvnmul  37860  dvnprodlem2  37864  salexct  38250  sge00  38277  sge0iunmpt  38319  meadjiun  38365  carageneld  38387  ovncvrrp  38449  ovolval4lem1  38534  aibandbiaiffaiffb  38572  plcofph  38623  pldofph  38624  plvcofph  38625  plvcofphax  38626  plvofpos  38627  aovov0bi  38789  icceuelpartlem  38840  rexdifpr  39087  ausgrusgrb  39352  cplgr3v  39604  uhgrvd0nedgb  39647  isrgr  39679  rgrusgrprc  39706  rgrprcx  39709  upgr2wlk  39767  umgrislfupgrlem  39770  usgfislem1  40081  usgfisALTlem1  40085  copisnmnd  40134  pgrpgt2nabl  40476  lindslinindsimp2lem5  40580  islininds2  40602  ldepslinc  40627
  Copyright terms: Public domain W3C validator