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

Theorem bicomi 194
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 191 . 2  |-  ( (
ph 
<->  ps )  ->  ( ps 
<-> 
ph ) )
31, 2ax-mp 8 1  |-  ( ps  <->  ph )
Colors of variables: wff set class
Syntax hints:    <-> wb 177
This theorem is referenced by:  biimpri  198  bitr2i  242  bitr3i  243  bitr4i  244  syl5bbr  251  syl5rbbr  252  syl6bbr  255  syl6rbbr  256  mtbir  291  sylnibr  297  sylnbir  299  xchnxbir  301  xchbinxr  303  con1bii  322  con2bii  323  nbn  337  xor3  347  pm5.41  354  pm4.64  362  pm4.63  411  pm4.61  416  anor  476  pm4.53  479  pm4.55  481  pm4.56  482  pm4.57  484  pm4.25  502  pm4.87  568  anidm  626  pm4.77  763  anabs1  784  anabs7  786  pm4.76  837  pm5.63  891  jaoi2  934  3ianor  951  3oran  953  pm3.2an3  1133  syl3anbr  1228  3an6  1264  nannot  1299  truimfal  1351  nottru  1354  nic-dfim  1440  nic-dfneg  1441  2nalexn  1579  sbid  1943  dvelimf  2050  cleljust  2064  cleljustALT  2065  sb10f  2172  nne  2571  necon3bbii  2598  necon2abii  2622  necon2bbii  2623  nnel  2665  alexeq  3025  ceqsrexbv  3030  clel2  3032  clel4  3035  2reu5lem1  3099  2reu5lem2  3100  2reu5lem3  3101  dfsbcq2  3124  cbvreucsf  3273  nss  3366  raldifb  3447  difab  3570  un0  3612  in0  3613  ss0b  3617  ssunsn2  3918  iindif2  4120  nssss  4379  epse  4525  uniuni  4675  cotr  5205  issref  5206  mptpreima  5322  ralrnmpt  5837  weniso  6034  eroveu  6958  isfinite2  7324  marypha1lem  7396  marypha2lem4  7401  en3lplem2  7627  carden2  7830  fseqenlem1  7861  iscard3  7930  cardnum  7931  alephinit  7932  cardinfima  7934  alephiso  7935  dfac10b  7975  dfackm  8002  isfin5-2  8227  brdom7disj  8365  brdom6disj  8366  hashtpg  11646  splfv1  11739  s4f1o  11820  vdwapun  13297  grpss  14781  drngnidl  16255  drnglpir  16279  unocv  16862  toptopon  16953  ordtbas2  17209  ordtrest2  17222  restutopopn  18221  xmeterval  18415  ovolfcl  19316  eldv  19738  eltayl  20229  musumsum  20930  usgrafilem1  21378  trls  21489  is2wlk  21518  lejdii  22993  mdslle1i  23773  mdslle2i  23774  mdslj1i  23775  mdslj2i  23776  mo5f  23925  unipreima  24009  2ndpreima  24049  ballotlem2  24699  relexpindlem  25092  fprod2dlem  25257  cnvco1  25331  cnvco2  25332  dfiota3  25676  nabi1i  26045  nabi2i  26046  trer  26209  inixp  26320  an43  26585  rmxypairf1o  26864  dsmmacl  27075  pmtrfrn  27268  acsfn1p  27375  pm10.252  27424  pm10.253  27425  pm10.42  27427  2nexaln  27441  aaanv  27455  pm13.195  27481  pm13.196a  27482  aibandbiaiffaiffb  27729  aovov0bi  27927  rexdifpr  27947  dff14a  27959  f13dfv  27962  el2wlkonotot0  28069  usg2spthonot0  28086  frgraun  28100  4cycl2vnunb  28121  vdn0frgrav2  28128  vdgn0frgrav2  28129  2spotdisj  28164  usg2spot2nb  28168  usgreg2spot  28170  sbc3org  28327  en3lpVD  28666  3orbi123VD  28671  sbc3orgVD  28672  undif3VD  28703  a9e2ndeqVD  28730  a9e2ndeqALT  28753  bnj115  28796  bnj156  28801  bnj206  28804  bnj110  28935  bnj121  28947  bnj124  28948  bnj130  28951  bnj153  28957  bnj207  28958  bnj581  28985  bnj611  28995  bnj864  28999  bnj865  29000  bnj893  29005  bnj1000  29018  bnj978  29026  bnj1040  29047  bnj1049  29049  bnj1133  29064  bnj1189  29084  cleljustNEW7  29328  dvelimfOLD7  29411  sb10fOLD7  29451  isopos  29663  islvol5  30061  elpadd0  30291  dvhopellsm  31600  diblsmopel  31654  mapdvalc  32112
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 178
  Copyright terms: Public domain W3C validator