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

Theorem bicomi 195
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 192 . 2  |-  ( (
ph 
<->  ps )  ->  ( ps 
<-> 
ph ) )
31, 2ax-mp 10 1  |-  ( ps  <->  ph )
Colors of variables: wff set class
Syntax hints:    <-> wb 178
This theorem is referenced by:  biimpri  199  bitr2i  243  bitr3i  244  bitr4i  245  syl5bbr  252  syl5rbbr  253  syl6bbr  256  syl6rbbr  257  mtbir  292  sylnibr  298  sylnbir  300  xchnxbir  302  xchbinxr  304  con1bii  323  con2bii  324  nbn  338  xor3  348  pm5.41  355  pm4.64  363  pm4.63  412  pm4.61  417  anor  477  pm4.53  480  pm4.55  482  pm4.56  483  pm4.57  485  pm4.25  503  pm4.87  570  anidm  628  pm4.77  765  anabs1  786  anabs7  788  pm4.76  841  pm5.63  895  3ianor  954  3oran  956  pm3.2an3  1136  syl3anbr  1231  3an6  1267  nannot  1298  truimfal  1341  nottru  1344  nic-dfim  1429  nic-dfneg  1430  2nalexn  1571  sbid  1895  dvelimf  1975  cleljust  2060  sb10f  2082  nne  2416  necon3bbii  2443  necon2abii  2467  necon2bbii  2468  alexeq  2834  ceqsrexbv  2839  clel2  2841  clel4  2844  dfsbcq2  2924  cbvreucsf  3073  nss  3157  difab  3344  un0  3386  in0  3387  ss0b  3391  ssunsn2  3673  iindif2  3869  nssss  4123  epse  4269  uniuni  4418  reusv2lem4  4429  cotr  4962  issref  4963  mptpreima  5072  ralrnmpt  5521  weniso  5704  eroveu  6639  isfinite2  7000  marypha1lem  7070  marypha2lem4  7075  en3lplem2  7301  carden2  7504  fseqenlem1  7535  iscard3  7604  cardnum  7605  alephinit  7606  cardinfima  7608  alephiso  7609  dfac10b  7649  dfackm  7676  isfin5-2  7901  brdom7disj  8040  brdom6disj  8041  splfv1  11347  vdwapun  12895  grpss  14338  drngnidl  15813  drnglpir  15837  unocv  16412  toptopon  16503  ordtbas2  16753  ordtrest2  16766  xmeterval  17810  ovolfcl  18658  eldv  19080  eltayl  19571  musumsum  20264  lejdii  21947  mdslle1i  22727  mdslle2i  22728  mdslj1i  22729  mdslj2i  22730  relexpindlem  23207  cnvco1  23287  cnvco2  23288  dfiota3  23636  funpartfv  23657  nabi1i  24004  nabi2i  24005  negcmpprcal2  24111  eqvinopb  24130  boxeq  24152  notev  24155  notal  24156  albineal  24164  splint  24213  restidsing  24241  imfstnrelc  24246  defse3  24438  qusp  24708  algi  24893  prismorcsetlemc  25083  nbssntrs  25313  trer  25393  inixp  25565  an43  25878  rmxypairf1o  26162  dsmmacl  26373  pmtrfrn  26566  acsfn1p  26673  pm10.252  26722  pm10.253  26723  pm10.42  26725  2nexaln  26739  aaanv  26753  pm13.195  26780  pm13.196a  26781  sbc3org  26988  en3lpVD  27311  3orbi123VD  27316  sbc3orgVD  27317  undif3VD  27348  a9e2ndeqVD  27375  a9e2ndeqALT  27398  bnj115  27440  bnj156  27445  bnj206  27448  bnj110  27579  bnj121  27591  bnj124  27592  bnj130  27595  bnj153  27601  bnj207  27602  bnj605  27628  bnj581  27629  bnj611  27639  bnj864  27643  bnj865  27644  bnj893  27649  bnj1000  27662  bnj978  27670  bnj1040  27691  bnj1049  27693  bnj1133  27708  bnj1189  27728  isopos  28059  islvol5  28457  elpadd0  28687  dvhopellsm  29996  diblsmopel  30050  mapdvalc  30508
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10
This theorem depends on definitions:  df-bi 179
  Copyright terms: Public domain W3C validator