Theorem bicomi 227

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

Syntax hints:   ↔ wb 209

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 210

This theorem is referenced by:  biimpri  231  bitr2i  279  bitr3i  280  bitr4i  281  bitr3id  288  bitr3di  289  bitr4di  292  bitr4id  293  mtbir  326  sylnibr  332  sylnbir  334  xchnxbir  336  xchbinxr  338  con1bii  360  nbn  376  xor3  387  pm5.41  395  pm4.63  401  pm4.61  408  pm4.76  522  anidm  568  an21  644  an43  658  anabs1  662  anabs7  664  pm4.87  842  pm4.64  848  pm4.25  905  pm4.77  962  pm4.53  985  pm4.55  987  pm4.56  988  pm4.57  990  pm5.63  1019  3anor  1109  3oran  1110  syl3anbr  1163  3an6  1447  nanbi  1495  nornot  1529  nororOLD  1534  truan  1553  truimfal  1566  nottru  1569  falbitru  1572  falnorfalOLD  1597  nic-dfim  1676  nic-dfneg  1677  2nalexn  1834  2nexaln  1836  equvinv  2041  cleljust  2123  sbelx  2255  sb5OLD  2277  sb6rfv  2359  cleljustALT  2365  cleljustALT2  2366  dvelimf  2449  sb5rf  2468  sb6rf  2469  sb10f  2533  nexmo  2542  cbvmovw  2604  exists2  2665  cleljustab  2720  abeq1i  2869  abbi2dv  2870  nfabdwOLD  2924  nne  2939  necon3bbii  2982  necon2abii  2985  necon2bbii  2986  nnel  3048  ralcom4  3149  nelb  3179  rspc2gv  3538  ceqsrexbv  3556  clel4OLD  3565  rabeqc  3591  2reu5lem1  3659  2reu5lem2  3660  2reu5lem3  3661  dfsbcq2  3688  cbvreucsf  3844  nss  3949  ss2abdv  3963  dfdif3  4015  symdifass  4152  indifdi  4184  difab  4200  neq0  4244  ab0OLD  4274  un0  4289  in0  4290  ss0b  4296  eq0rdv  4303  2nreu  4341  ralidm  4408  ralf0  4410  rexdifpr  4559  reuprg  4604  ssunsn2  4725  iindif2  4972  nssss  5324  snopeqop  5373  epse  5518  rnep  5780  cotrg  5955  mptpreima  6080  ralrnmpt  6885  fmptsng  6953  fmptsnd  6954  dff14a  7052  f13dfv  7055  weniso  7133  abnex  7511  uniuni  7516  suppvalbr  7873  eroveu  8436  fsetexb  8487  mapsnend  8648  isfinite2  8863  marypha1lem  8983  marypha2lem4  8988  infcllem  9037  en3lplem2  9162  cantnfp1  9230  carden2  9502  fseqenlem1  9537  iscard3  9606  cardnum  9607  alephinit  9608  cardinfima  9610  alephiso  9611  dfac10b  9652  dfackm  9679  isfin5-2  9904  brdom7disj  10044  brdom6disj  10045  fsuppmapnn0fiubex  13464  hash2prb  13937  hashle2prv  13943  hashtpg  13950  swrdnnn0nd  14120  wrd2ind  14187  cshwsexa  14288  s4f1o  14382  cotr2g  14438  relexpindlem  14525  lcmfunsnlem2  16094  ncoprmlnprm  16181  vdwapun  16423  cshwsiun  16549  cshwshash  16554  grpss  18252  symgsubmefmnd  18657  pmtrfrn  18717  pmtrrn2  18719  pmtrprfvalrn  18747  issrg  19389  acsfn1p  19710  0ringnnzr  20174  unocv  20509  dsmmacl  20570  pmatcollpw2lem  21541  fvmptnn04if  21613  toptopon  21681  ordtbas2  21955  ordtrest2  21968  xmeterval  23198  isclmp  23862  ovolfcl  24231  eldv  24663  eltayl  25120  musumsum  25942  2sqreu  26205  2sqreunn  26206  2sqreult  26207  2sqreultb  26208  2sqreunnlt  26209  2sqreunnltb  26210  umgrislfupgrlem  27080  numedglnl  27102  ausgrusgrb  27123  cplgr3v  27390  vtxd0nedgb  27443  finsumvtxdg2ssteplem1  27500  isrgr  27514  rgrusgrprc  27544  rgrprcx  27547  upgr2wlk  27623  pthsfval  27675  wwlksnwwlksnon  27866  usgr2wspthon  27916  isclwwlk  27934  clwwlkvbij  28063  iseupthf1o  28152  frcond2  28217  nfrgr2v  28222  4cycl2vnunb  28240  fusgr2wsp2nb  28284  frgrregord013  28345  lejdii  29486  mdslle1i  30265  mdslle2i  30266  mdslj1i  30267  mdslj2i  30268  mo5f  30424  unipreima  30568  2ndpreima  30628  mgccnv  30867  quslsm  31178  ordtrest2NEW  31458  ordtconnlem1  31459  ballotlem2  32038  plymulx0  32109  bnj115  32287  bnj156  32290  bnj206  32293  bnj110  32422  bnj121  32434  bnj124  32435  bnj130  32438  bnj153  32444  bnj207  32445  bnj581  32472  bnj611  32482  bnj864  32486  bnj865  32487  bnj893  32492  bnj1000  32505  bnj978  32513  bnj1040  32536  bnj1049  32538  bnj1133  32553  bnj1189  32573  satfv1  32909  satfvsucsuc  32911  satfdm  32915  satf0  32918  satf0op  32923  fmlafvel  32931  cnvco1  33313  cnvco2  33314  nosupinfsep  33591  dfiota3  33881  trer  34161  nabi1i  34239  nabi2i  34240  bj-hbext  34548  bj-nnfbit  34590  bj-dvelimdv  34691  bj-gabima  34784  bj-elsngl  34814  bj-nuliotaALT  34885  bj-rest10  34913  bj-restuni  34922  con1bii2  35159  con2bii2  35160  topdifinfeq  35177  isbasisrelowllem2  35183  wl-1xor  35309  wl-1mintru1  35315  wl-sb8eut  35388  inixp  35542  notbinot1  35893  notbinot2  35897  truconj  35915  sbccom2lem  35938  sbccom2  35939  sbccom2f  35940  tsim1  35944  tsxo3  35953  tsxo4  35954  trcoss2  36258  dfmember3  36442  eqvreldmqs  36443  isopos  36850  islvol5  37249  elpadd0  37479  dvhopellsm  38787  diblsmopel  38841  mapdvalc  39299  3factsumint2  39683  3factsumint3  39684  3factsumint4  39685  aks4d1p1p2  39730  elpwbi  39828  dffltz  40084  rmxypairf1o  40346  ifpnotnotb  40681  ifpdfxor  40689  ifpidg  40693  ifpim123g  40702  ifpim1g  40703  ifpimimb  40706  ifpimim  40711  rp-fakeanorass  40715  elmapintrab  40770  undmrnresiss  40798  clcnvlem  40817  sqrtcvallem1  40825  cnviun  40845  dfxor4  40961  dfhe3  40970  dffrege69  41127  dffrege76  41134  or3or  41218  uneqsn  41220  scottabf  41441  mnurndlem1  41482  pm10.252  41558  pm10.253  41559  pm10.42  41561  aaanv  41585  pm13.195  41610  pm13.196a  41611  sbc3or  41731  en3lpVD  42044  3orbi123VD  42049  sbc3orgVD  42050  sbcoreleleqVD  42058  undif3VD  42081  ax6e2ndeqVD  42108  ax6e2ndeqALT  42130  sineq0ALT  42136  uzwo4  42180  fompt  42309  allbutfiinf  42539  limsupequzmptlem  42852  cncfshift  42998  dvnmul  43067  dvnprodlem2  43071  rrxsnicc  43424  salexct  43456  sge00  43497  sge0iunmpt  43539  meadjiun  43587  carageneld  43623  ovncvrrp  43685  ovolval4lem1  43770  vonioo  43803  vonicc  43806  nsssmfmbf  43894  smfmullem4  43908  aibandbiaiffaiffb  43969  plcofph  44019  pldofph  44020  plvcofph  44021  plvcofphax  44022  plvofpos  44023  fsetsniunop  44123  2reu8i  44186  aovov0bi  44269  tz6.12-afv2  44313  4an21  44343  ichbi12i  44494  ichnfimlem  44497  spr0nelg  44510  sprvalpwn0  44517  reuprpr  44557  requad2  44657  copisnmnd  44945  pgrpgt2nabl  45284  lindslinindsimp2lem5  45385  islininds2  45407  ldepslinc  45432  line2ylem  45679