Theorem bicomi 214

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

Step	Hyp	Ref	Expression
1		bicomi.1	. 2 |- ( ph <-> ps )
2		bicom1 211	. 2 |- ( ( ph <-> ps ) -> ( ps <-> ph ) )
3	1, 2	ax-mp 5	1 |- ( ps <-> ph )

Syntax hints:   <-> wb 196

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 197

This theorem is referenced by:  biimpri  218  bitr2i  265  bitr3i  266  bitr4i  267  syl5bbr  274  syl5rbbr  275  syl6bbr  278  syl6rbbr  279  mtbir  313  sylnibr  319  sylnbir  321  xchnxbir  323  xchbinxr  325  con1bii  346  con2bii  347  nbn  362  xor3  372  pm5.41  379  pm4.64  387  pm4.63  437  pm4.61  442  anor  510  pm4.53  513  pm4.55  515  pm4.56  516  pm4.57  518  pm4.25  537  pm4.87  608  anidm  676  pm4.77  828  anabs1  850  anabs7  852  an43  867  pm4.76  910  pm5.63  959  3ianor  1055  3oran  1057  pm3.2an3OLD  1241  syl3anbr  1370  3an6  1409  nannot  1453  nanbi  1454  truan  1501  truimfal  1515  nottru  1518  falbitru  1521  nic-dfim  1594  nic-dfneg  1595  2nalexn  1755  2nexaln  1757  sbequ8  1885  cleljust  1998  cleljustALT  2185  cleljustALT2  2186  dvelimf  2334  sb5rf  2422  sb6rf  2423  sb10f  2456  abeq1i  2736  nne  2798  necon3bbii  2841  necon2abii  2844  necon2bbii  2845  nnel  2906  rspc2gv  3321  ceqsrexbv  3337  clel2  3339  clel4  3342  2reu5lem1  3413  2reu5lem2  3414  2reu5lem3  3415  dfsbcq2  3438  cbvreucsf  3567  nss  3663  difab  3896  un0  3967  in0  3968  ss0b  3973  rexdifpr  4205  ssdifsn  4318  ssunsn2  4359  iindif2  4589  nssss  4924  epse  5097  restidsingOLD  5459  cotrg  5507  issref  5509  mptpreima  5628  ralrnmpt  6368  fmptsng  6434  fmptsnd  6435  dff14a  6527  f13dfv  6530  weniso  6604  abnex  6965  uniuni  6971  suppvalbr  7299  eroveu  7842  isfinite2  8218  marypha1lem  8339  marypha2lem4  8344  infcllem  8393  wemapso2lem  8457  en3lplem2  8512  cantnfp1  8578  carden2  8813  fseqenlem1  8847  iscard3  8916  cardnum  8917  alephinit  8918  cardinfima  8920  alephiso  8921  dfac10b  8961  dfackm  8988  isfin5-2  9213  brdom7disj  9353  brdom6disj  9354  fsuppmapnn0fiubex  12792  hash2prb  13254  hashle2prv  13260  hashtpg  13267  wrd2ind  13477  splfv1  13506  cshwsexa  13570  s4f1o  13663  cotr2g  13715  relexpindlem  13803  lcmfunsnlem2  15353  ncoprmlnprm  15436  vdwapun  15678  cshwsiun  15806  cshwshash  15811  grpss  17440  pmtrfrn  17878  pmtrrn2  17880  pmtrprfvalrn  17908  issrg  18507  drngnidl  19229  drnglpir  19253  0ringnnzr  19269  unocv  20024  dsmmacl  20085  pmatcollpw2lem  20582  fvmptnn04if  20654  toptopon  20722  toprntopon  20729  ordtbas2  20995  ordtrest2  21008  xmeterval  22237  isclmp  22897  ovolfcl  23235  eldv  23662  eltayl  24114  musumsum  24918  umgrislfupgrlem  26017  numedglnl  26039  ausgrusgrb  26060  cplgr3v  26331  vtxd0nedgb  26384  finsumvtxdg2ssteplem1  26441  isrgr  26455  rgrusgrprc  26485  rgrprcx  26488  upgr2wlk  26564  pthsfval  26617  wlksnwwlknvbij  26803  usgr2wspthon  26858  isclwwlks  26880  clwwlksvbij  26922  iseupthf1o  27062  frcond2  27131  nfrgr2v  27136  4cycl2vnunb  27154  fusgr2wsp2nb  27198  frgrregord013  27253  lejdii  28397  mdslle1i  29176  mdslle2i  29177  mdslj1i  29178  mdslj2i  29179  mo5f  29324  unipreima  29446  2ndpreima  29485  ordtrest2NEW  29969  ordtconnlem1  29970  ballotlem2  30550  plymulx0  30624  bnj115  30791  bnj156  30796  bnj206  30799  bnj110  30928  bnj121  30940  bnj124  30941  bnj130  30944  bnj153  30950  bnj207  30951  bnj581  30978  bnj611  30988  bnj864  30992  bnj865  30993  bnj893  30998  bnj1000  31011  bnj978  31019  bnj1040  31040  bnj1049  31042  bnj1133  31057  bnj1189  31077  cnvco1  31649  cnvco2  31650  dfiota3  32030  trer  32310  nabi1i  32391  nabi2i  32392  bj-dfifc2  32564  bj-df-ifc  32565  bj-dfssb2  32640  bj-hbext  32701  bj-dvelimdv  32834  bj-cleljustab  32847  bj-denotes  32858  bj-ralcom4  32868  bj-rexcom4  32869  bj-elsngl  32956  bj-nuliotaALT  33020  bj-rest10  33041  bj-restuni  33050  bj-ismooredr2  33065  con1bii2  33179  con2bii2  33180  topdifinfeq  33198  isbasisrelowllem2  33204  wl-sb8eut  33359  wl-clelv2-just  33379  inixp  33523  notbinot1  33878  notbinot2  33882  truconj  33903  sbccom2lem  33929  sbccom2  33930  sbccom2f  33931  tsim1  33937  tsxo3  33946  tsxo4  33947  isopos  34467  islvol5  34865  elpadd0  35095  dvhopellsm  36406  diblsmopel  36460  mapdvalc  36918  rmxypairf1o  37476  acsfn1p  37769  ifpnotnotb  37824  ifpdfxor  37832  ifpidg  37836  ifpim123g  37845  ifpim1g  37846  ifpimimb  37849  ifpimim  37854  rp-fakeanorass  37858  rp-isfinite6  37864  elmapintrab  37882  undmrnresiss  37910  clcnvlem  37930  cnviun  37942  dfxor4  38058  dfhe3  38069  dffrege69  38226  dffrege76  38233  or3or  38319  uneqsn  38321  pm10.252  38560  pm10.253  38561  pm10.42  38563  aaanv  38588  pm13.195  38614  pm13.196a  38615  sbc3or  38738  sbc3orgOLD  38742  en3lpVD  39080  3orbi123VD  39085  sbc3orgVD  39086  undif3VD  39118  ax6e2ndeqVD  39145  ax6e2ndeqALT  39167  sineq0ALT  39173  uzwo4  39221  rnmptpr  39358  fompt  39379  mapsnend  39391  allbutfiinf  39647  limsupequzmptlem  39960  cncfshift  40087  dvnmul  40158  dvnprodlem2  40162  rrxsnicc  40520  salexct  40552  sge00  40593  sge0iunmpt  40635  meadjiun  40683  carageneld  40716  ovncvrrp  40778  ovolval4lem1  40863  vonioo  40896  vonicc  40899  nsssmfmbf  40987  smfmullem4  41001  aibandbiaiffaiffb  41061  plcofph  41111  pldofph  41112  plvcofph  41113  plvcofphax  41114  plvofpos  41115  aovov0bi  41276  spr0nelg  41726  sprvalpwn0  41733  copisnmnd  41809  pgrpgt2nabl  42147  lindslinindsimp2lem5  42251  islininds2  42273  ldepslinc  42298