Theorem bicomi 213

Description: Inference from commutative law for logical equivalence. (Contributed by NM, 3-Jan-1993.)

Hypothesis

Ref	Expression
bicomi.1	⊢ (𝜑 ↔ 𝜓)

Assertion

Ref	Expression
bicomi	⊢ (𝜓 ↔ 𝜑)

Proof of Theorem bicomi

Step	Hyp	Ref	Expression
1		bicomi.1	. 2 ⊢ (𝜑 ↔ 𝜓)
2		bicom1 210	. 2 ⊢ ((𝜑 ↔ 𝜓) → (𝜓 ↔ 𝜑))
3	1, 2	ax-mp 5	1 ⊢ (𝜓 ↔ 𝜑)

Syntax hints:   ↔ wb 195

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 196

This theorem is referenced by:  biimpri  217  bitr2i  264  bitr3i  265  bitr4i  266  syl5bbr  273  syl5rbbr  274  syl6bbr  277  syl6rbbr  278  mtbir  312  sylnibr  318  sylnbir  320  xchnxbir  322  xchbinxr  324  con1bii  345  con2bii  346  nbn  361  xor3  371  pm5.41  378  pm4.64  386  pm4.63  436  pm4.61  441  anor  509  pm4.53  512  pm4.55  514  pm4.56  515  pm4.57  517  pm4.25  536  pm4.87  606  anidm  674  pm4.77  824  anabs1  846  anabs7  848  an43  863  pm4.76  906  pm5.63  961  3ianor  1048  3oran  1050  pm3.2an3OLD  1234  syl3anbr  1362  3an6  1401  nannot  1445  nanbi  1446  truan  1492  truimfal  1506  nottru  1509  falbitru  1512  nic-dfim  1585  nic-dfneg  1586  2nalexn  1745  2nexaln  1747  sbequ8  1872  cleljust  1985  cleljustALT  2173  cleljustALT2  2174  dvelimf  2322  sb5rf  2410  sb6rf  2411  sb10f  2444  abeq1i  2723  nne  2786  necon3bbii  2829  necon2abii  2832  necon2bbii  2833  nnel  2892  ceqsrexbv  3307  clel2  3309  clel4  3312  2reu5lem1  3380  2reu5lem2  3381  2reu5lem3  3382  dfsbcq2  3405  cbvreucsf  3533  nss  3626  difab  3855  un0  3919  in0  3920  ss0b  3925  ssunsn2  4299  iindif2  4525  nssss  4851  epse  5021  restidsingOLD  5378  cotrg  5426  issref  5428  mptpreima  5545  ralrnmpt  6276  fmptsng  6339  fmptsnd  6340  dff14a  6427  f13dfv  6430  weniso  6504  fvmptopab2  6595  uniuni  6865  suppvalbr  7186  eroveu  7729  isfinite2  8103  marypha1lem  8222  marypha2lem4  8227  infcllem  8276  wemapso2lem  8340  en3lplem2  8395  cantnfp1  8461  carden2  8696  fseqenlem1  8730  iscard3  8799  cardnum  8800  alephinit  8801  cardinfima  8803  alephiso  8804  dfac10b  8844  dfackm  8871  isfin5-2  9096  brdom7disj  9234  brdom6disj  9235  fsuppmapnn0fiubex  12654  hash2prb  13111  hashtpg  13121  wrd2ind  13329  splfv1  13357  cshwsexa  13421  s4f1o  13513  cotr2g  13563  relexpindlem  13651  lcmfunsnlem2  15191  ncoprmlnprm  15274  vdwapun  15516  cshwsiun  15644  cshwshash  15649  grpss  17263  pmtrfrn  17701  pmtrrn2  17703  pmtrprfvalrn  17731  issrg  18330  drngnidl  19050  drnglpir  19074  0ringnnzr  19090  unocv  19843  dsmmacl  19904  pmatcollpw2lem  20401  fvmptnn04if  20473  toptopon  20548  ordtbas2  20805  ordtrest2  20818  xmeterval  22047  isclmp  22705  ovolfcl  23042  eldv  23468  eltayl  23918  musumsum  24718  umgrislfupgrlem  25788  usgrafilem1  25940  trls  26066  is2wlk  26095  wwlknndef  26265  wlknwwlknvbij  26268  clwwlknndef  26301  clwwlkvbij  26329  el2wlkonotot0  26399  usg2spthonot0  26416  frgraun  26523  frgra2v  26526  4cycl2vnunb  26544  vdn0frgrav2  26550  vdgn0frgrav2  26551  2spotdisj  26588  usg2spot2nb  26592  usgreg2spot  26594  frgraregord013  26645  lejdii  27781  mdslle1i  28560  mdslle2i  28561  mdslj1i  28562  mdslj2i  28563  mo5f  28708  unipreima  28826  2ndpreima  28868  ordtrest2NEW  29297  ordtconlem1  29298  ballotlem2  29877  plymulx0  29950  bnj115  30045  bnj156  30050  bnj206  30053  bnj110  30182  bnj121  30194  bnj124  30195  bnj130  30198  bnj153  30204  bnj207  30205  bnj581  30232  bnj611  30242  bnj864  30246  bnj865  30247  bnj893  30252  bnj1000  30265  bnj978  30273  bnj1040  30294  bnj1049  30296  bnj1133  30311  bnj1189  30331  cnvco1  30903  cnvco2  30904  dfiota3  31200  trer  31480  nabi1i  31561  nabi2i  31562  bj-dfifc2  31734  bj-df-ifc  31735  bj-nf3  31767  bj-dfssb2  31829  bj-hbext  31888  bj-dvelimdv  32027  bj-denotes  32052  bj-ralcom4  32062  bj-rexcom4  32063  bj-elsngl  32149  bj-nuliotaALT  32211  bj-rest10  32222  bj-restuni  32231  bj-sspwpw  32238  bj-toprntopon  32244  con1bii2  32355  con2bii2  32356  topdifinfeq  32374  isbasisrelowllem2  32380  wl-sb8eut  32538  inixp  32693  notbinot1  33048  notbinot2  33052  truconj  33073  sbccom2lem  33099  sbccom2  33100  sbccom2f  33101  tsim1  33107  tsxo3  33116  tsxo4  33117  isopos  33485  islvol5  33883  elpadd0  34113  dvhopellsm  35424  diblsmopel  35478  mapdvalc  35936  rmxypairf1o  36494  acsfn1p  36788  ifpnotnotb  36843  ifpdfxor  36851  ifpidg  36855  ifpim123g  36864  ifpim1g  36865  ifpimimb  36868  ifpimim  36873  rp-fakeanorass  36877  rp-isfinite6  36883  elmapintrab  36901  undmrnresiss  36929  clcnvlem  36949  cnviun  36961  dfxor4  37077  dfhe3  37089  dffrege69  37246  dffrege76  37253  or3or  37339  uneqsn  37341  pm10.252  37582  pm10.253  37583  pm10.42  37585  aaanv  37610  pm13.195  37636  pm13.196a  37637  sbc3or  37759  sbc3orgOLD  37763  en3lpVD  38102  3orbi123VD  38107  sbc3orgVD  38108  undif3VD  38140  ax6e2ndeqVD  38167  ax6e2ndeqALT  38189  sineq0ALT  38195  uzwo4  38246  inn0f  38268  rnmptpr  38353  fompt  38374  mapsnend  38386  cncfshift  38759  dvnmul  38833  dvnprodlem2  38837  rrxsnicc  39196  salexct  39228  sge00  39269  sge0iunmpt  39311  meadjiun  39359  carageneld  39392  ovncvrrp  39454  ovolval4lem1  39539  vonioo  39573  vonicc  39576  nsssmfmbf  39665  smfmullem4  39679  aibandbiaiffaiffb  39710  plcofph  39760  pldofph  39761  plvcofph  39762  plvcofphax  39763  plvofpos  39764  aovov0bi  39925  rexdifpr  40315  ausgrusgrb  40395  cplgr3v  40657  vtxd0nedgb  40703  isrgr  40759  rgrusgrprc  40789  rgrprcx  40792  upgr2wlk  40876  wlksnwwlknvbij  41114  usgr2wspthon  41168  isclwwlks  41188  clwwlksvbij  41229  frcond2  41439  nfrgr2v  41442  4cycl2vnunb-av  41460  fusgr2wsp2nb  41498  av-frgraregord013  41549  copisnmnd  41599  pgrpgt2nabl  41941  lindslinindsimp2lem5  42045  islininds2  42067  ldepslinc  42092  ssdifsn  42228