Theorem bicomi 216

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 213	. 2 ⊢ ((𝜑 ↔ 𝜓) → (𝜓 ↔ 𝜑))
3	1, 2	ax-mp 5	1 ⊢ (𝜓 ↔ 𝜑)

Syntax hints:   ↔ wb 198

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 199

This theorem is referenced by:  biimpri  220  bitr2i  268  bitr3i  269  bitr4i  270  syl5bbr  277  syl5rbbr  278  syl6bbr  281  syl6rbbr  282  mtbir  315  sylnibr  321  sylnbir  323  xchnxbir  325  xchbinxr  327  con1bii  348  con2bii  349  nbn  364  xor3  374  pm5.41  382  pm4.63  388  pm4.61  395  pm4.76  516  anidm  562  an43  650  anabs1  654  anabs7  656  pm4.87  876  pm4.64  882  pm4.25  936  pm4.77  992  anor  1012  pm4.53  1015  pm4.55  1017  pm4.56  1018  pm4.57  1020  pm5.63  1050  3anor  1139  3ianorOLD  1140  3oran  1141  syl3anbr  1207  3an6  1576  nannotOLD  1625  nanbi  1626  truan  1670  truimfal  1683  nottru  1686  falbitru  1689  nic-dfim  1770  nic-dfneg  1771  2nalexn  1928  2nexaln  1930  sbequ8  2074  equvinv  2136  cleljust  2174  sb6rfv  2381  cleljustALT  2385  cleljustALT2  2386  dvelimf  2468  sb5rf  2553  sb6rf  2554  sb10f  2589  nexmo  2605  eu6OLD  2646  moeuOLD  2670  exists2  2743  nulmo  2809  abeq1i  2940  nne  3002  necon3bbii  3045  necon2abii  3048  necon2bbii  3049  nnel  3110  rspc2gv  3537  ceqsrexbv  3554  clel4  3560  rabeqc  3582  2reu5lem1  3639  2reu5lem2  3640  2reu5lem3  3641  dfsbcq2  3664  cbvreucsf  3790  nss  3887  dfdif3  3946  symdifass  4078  difab  4124  un0  4191  in0  4192  ss0b  4197  rexdifpr  4425  ssdifsnOLD  4537  ssunsn2  4575  iindif2  4808  nssss  5144  snopeqop  5190  epse  5324  cotrg  5747  idrefOLD  5750  mptpreima  5868  ralrnmpt  6616  fmptsng  6685  fmptsnd  6686  dff14a  6781  f13dfv  6784  weniso  6858  abnex  7225  uniuni  7230  suppvalbr  7562  eroveu  8107  mapsnend  8300  isfinite2  8486  marypha1lem  8607  marypha2lem4  8612  infcllem  8661  wemapso2lem  8725  en3lplem2  8784  cantnfp1  8854  carden2  9125  fseqenlem1  9159  iscard3  9228  cardnum  9229  alephinit  9230  cardinfima  9232  alephiso  9233  dfac10b  9275  dfackm  9302  isfin5-2  9527  brdom7disj  9667  brdom6disj  9668  fsuppmapnn0fiubex  13085  hash2prb  13542  hashle2prv  13548  hashtpg  13555  swrdnnn0nd  13720  wrd2ind  13813  wrd2indOLD  13814  splfv1  13867  splfv1OLD  13868  cshwsexa  13944  s4f1o  14038  cotr2g  14093  relexpindlem  14179  lcmfunsnlem2  15725  ncoprmlnprm  15806  vdwapun  16048  cshwsiun  16171  cshwshash  16176  grpss  17793  pmtrfrn  18227  pmtrrn2  18229  pmtrprfvalrn  18257  issrg  18860  drngnidl  19589  drnglpir  19613  0ringnnzr  19629  unocv  20386  dsmmacl  20447  pmatcollpw2lem  20951  fvmptnn04if  21023  toptopon  21091  toprntopon  21099  ordtbas2  21365  ordtrest2  21378  xmeterval  22606  isclmp  23265  ovolfcl  23631  eldv  24060  eltayl  24512  musumsum  25330  umgrislfupgrlem  26419  numedglnl  26442  ausgrusgrb  26463  cplgr3v  26732  vtxd0nedgb  26785  finsumvtxdg2ssteplem1  26842  isrgr  26856  rgrusgrprc  26886  rgrprcx  26889  upgr2wlk  26964  pthsfval  27022  wlksnwwlknvbijOLD  27230  wwlksnwwlksnon  27243  usgr2wspthon  27293  isclwwlk  27312  clwwlkvbij  27487  clwwlkvbijOLD  27488  iseupthf1o  27577  frcond2  27647  nfrgr2v  27652  4cycl2vnunb  27670  fusgr2wsp2nb  27714  frgrregord013  27809  lejdii  28951  mdslle1i  29730  mdslle2i  29731  mdslj1i  29732  mdslj2i  29733  mo5f  29878  unipreima  29994  2ndpreima  30032  ordtrest2NEW  30513  ordtconnlem1  30514  ballotlem2  31095  plymulx0  31170  bnj115  31339  bnj156  31342  bnj206  31345  bnj110  31473  bnj121  31485  bnj124  31486  bnj130  31489  bnj153  31495  bnj207  31496  bnj581  31523  bnj611  31533  bnj864  31537  bnj865  31538  bnj893  31543  bnj1000  31556  bnj978  31564  bnj1040  31585  bnj1049  31587  bnj1133  31602  bnj1189  31622  cnvco1  32190  cnvco2  32191  dfiota3  32568  trer  32848  nabi1i  32926  nabi2i  32927  bj-dfifc2  33092  bj-df-ifc  33093  bj-dfssb2  33175  bj-hbext  33234  bj-dvelimdv  33356  bj-cleljustab  33370  bj-denotes  33376  bj-ralcom4  33387  bj-rexcom4  33388  bj-elsngl  33477  bj-nuliotaALT  33541  bj-rest10  33563  bj-restuni  33572  bj-ismooredr2  33587  con1bii2  33724  con2bii2  33725  topdifinfeq  33742  isbasisrelowllem2  33748  wl-sb8eut  33902  wl-clelv2-just  33921  inixp  34065  notbinot1  34419  notbinot2  34423  truconj  34443  sbccom2lem  34468  sbccom2  34469  sbccom2f  34470  tsim1  34476  tsxo3  34485  tsxo4  34486  trcoss2  34781  isopos  35254  islvol5  35653  elpadd0  35883  dvhopellsm  37191  diblsmopel  37245  mapdvalc  37703  elpwbi  38043  dffltz  38096  rmxypairf1o  38318  acsfn1p  38611  ifpnotnotb  38665  ifpdfxor  38673  ifpidg  38677  ifpim123g  38686  ifpim1g  38687  ifpimimb  38690  ifpimim  38695  rp-fakeanorass  38699  rp-isfinite6  38704  elmapintrab  38722  undmrnresiss  38750  clcnvlem  38770  cnviun  38782  dfxor4  38898  dfhe3  38908  dffrege69  39065  dffrege76  39072  or3or  39158  uneqsn  39160  pm10.252  39399  pm10.253  39400  pm10.42  39402  aaanv  39427  pm13.195  39452  pm13.196a  39453  sbc3or  39575  en3lpVD  39898  3orbi123VD  39903  sbc3orgVD  39904  sbcoreleleqVD  39912  undif3VD  39935  ax6e2ndeqVD  39962  ax6e2ndeqALT  39984  sineq0ALT  39990  uzwo4  40037  rnmptpr  40166  fompt  40186  allbutfiinf  40441  limsupequzmptlem  40754  cncfshift  40881  dvnmul  40952  dvnprodlem2  40956  rrxsnicc  41310  salexct  41342  sge00  41383  sge0iunmpt  41425  meadjiun  41473  carageneld  41509  ovncvrrp  41571  ovolval4lem1  41656  vonioo  41689  vonicc  41692  nsssmfmbf  41780  smfmullem4  41794  aibandbiaiffaiffb  41854  plcofph  41904  pldofph  41905  plvcofph  41906  plvcofphax  41907  plvofpos  41908  aovov0bi  42097  tz6.12-afv2  42141  4an21  42171  spr0nelg  42572  sprvalpwn0  42579  copisnmnd  42655  pgrpgt2nabl  42993  lindslinindsimp2lem5  43097  islininds2  43119  ldepslinc  43144  line2ylem  43302