Theorem bicomi 223

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

Syntax hints:   ↔ wb 205

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 206

This theorem is referenced by:  biimpri  227  bitr2i  275  bitr3i  276  bitr4i  277  bitr3id  284  bitr3di  285  bitr4di  288  bitr4id  289  mtbir  322  sylnibr  328  sylnbir  330  xchnxbir  332  xchbinxr  334  con1bii  356  nbn  372  xor3  383  pm5.41  391  pm4.63  397  pm4.61  404  pm4.76  518  anidm  564  an21  640  an43  654  anabs1  658  anabs7  660  pm4.87  839  pm4.64  845  pm4.25  902  pm4.77  959  pm4.53  982  pm4.55  984  pm4.56  985  pm4.57  987  pm5.63  1016  3anor  1106  3oran  1107  syl3anbr  1160  3an6  1444  nanbi  1492  nornot  1526  nororOLD  1531  truan  1550  truimfal  1563  nottru  1566  falbitru  1569  falnorfalOLD  1594  nic-dfim  1673  nic-dfneg  1674  2nalexn  1831  2nexaln  1833  equvinv  2033  cleljust  2117  sbelx  2249  sb5OLD  2272  sb6rfv  2355  cleljustALT  2362  cleljustALT2  2363  dvelimf  2448  sb5rf  2467  sb6rf  2468  sb10f  2532  nexmo  2541  exists2  2663  cleljustab  2718  abeq1i  2875  abbi2dv  2876  nfabdwOLD  2930  nne  2946  necon3bbii  2990  necon2abii  2993  necon2bbii  2994  nnel  3057  ralcom4OLD  3162  nelbOLD  3195  rspc2gv  3561  ceqsrexbv  3579  clel4OLD  3588  rabeqc  3615  2reu5lem1  3685  2reu5lem2  3686  2reu5lem3  3687  dfsbcq2  3714  cbvreucsf  3875  nss  3979  ss2abdv  3993  dfdif3  4045  symdifass  4182  indifdi  4214  difab  4231  neq0  4276  ab0OLD  4306  un0  4321  in0  4322  ss0b  4328  eq0rdv  4335  2nreu  4372  ralidm  4439  ralf0  4441  rexdifpr  4591  reuprg  4636  ssunsn2  4757  iindif2  5002  eqsnuniex  5278  nssss  5365  snopeqop  5414  dffr6  5538  epse  5563  rnep  5825  cotrg  6005  mptpreima  6130  ralrnmpt  6954  fmptsng  7022  fmptsnd  7023  dff14a  7124  f13dfv  7127  weniso  7205  abnex  7585  uniuni  7590  suppvalbr  7952  eroveu  8559  fsetexb  8610  mapsnend  8780  isfinite2  9002  marypha1lem  9122  marypha2lem4  9127  infcllem  9176  en3lplem2  9301  cantnfp1  9369  carden2  9676  fseqenlem1  9711  iscard3  9780  cardnum  9781  alephinit  9782  cardinfima  9784  alephiso  9785  dfac10b  9826  dfackm  9853  isfin5-2  10078  brdom7disj  10218  brdom6disj  10219  fsuppmapnn0fiubex  13640  hash2prb  14114  hashle2prv  14120  hashtpg  14127  swrdnnn0nd  14297  wrd2ind  14364  cshwsexa  14465  s4f1o  14559  cotr2g  14615  relexpindlem  14702  lcmfunsnlem2  16273  ncoprmlnprm  16360  vdwapun  16603  cshwsiun  16729  cshwshash  16734  grpss  18512  symgsubmefmnd  18921  pmtrfrn  18981  pmtrrn2  18983  pmtrprfvalrn  19011  issrg  19658  acsfn1p  19982  0ringnnzr  20453  unocv  20797  dsmmacl  20858  pmatcollpw2lem  21834  fvmptnn04if  21906  toptopon  21974  ordtbas2  22250  ordtrest2  22263  xmeterval  23493  isclmp  24166  ovolfcl  24535  eldv  24967  eltayl  25424  musumsum  26246  2sqreu  26509  2sqreunn  26510  2sqreult  26511  2sqreultb  26512  2sqreunnlt  26513  2sqreunnltb  26514  umgrislfupgrlem  27395  numedglnl  27417  ausgrusgrb  27438  cplgr3v  27705  vtxd0nedgb  27758  finsumvtxdg2ssteplem1  27815  isrgr  27829  rgrusgrprc  27859  rgrprcx  27862  upgr2wlk  27938  pthsfval  27990  wwlksnwwlksnon  28181  usgr2wspthon  28231  isclwwlk  28249  clwwlkvbij  28378  iseupthf1o  28467  frcond2  28532  nfrgr2v  28537  4cycl2vnunb  28555  fusgr2wsp2nb  28599  frgrregord013  28660  lejdii  29801  mdslle1i  30580  mdslle2i  30581  mdslj1i  30582  mdslj2i  30583  mo5f  30738  unipreima  30882  2ndpreima  30942  mgccnv  31179  quslsm  31495  ordtrest2NEW  31775  ordtconnlem1  31776  ballotlem2  32355  plymulx0  32426  bnj115  32604  bnj156  32607  bnj206  32610  bnj110  32738  bnj121  32750  bnj124  32751  bnj130  32754  bnj153  32760  bnj207  32761  bnj581  32788  bnj611  32798  bnj864  32802  bnj865  32803  bnj893  32808  bnj1000  32821  bnj978  32829  bnj1040  32852  bnj1049  32854  bnj1133  32869  bnj1189  32889  satfv1  33225  satfvsucsuc  33227  satfdm  33231  satf0  33234  satf0op  33239  fmlafvel  33247  cnvco1  33632  cnvco2  33633  nosupinfsep  33862  dfiota3  34152  trer  34432  nabi1i  34510  nabi2i  34511  bj-hbext  34819  bj-nnfbit  34861  bj-dvelimdv  34962  bj-gabima  35055  bj-elsngl  35085  bj-nuliotaALT  35156  bj-rest10  35186  bj-restuni  35195  con1bii2  35430  con2bii2  35431  topdifinfeq  35448  isbasisrelowllem2  35454  wl-1xor  35580  wl-1mintru1  35586  wl-sb8eut  35659  inixp  35813  notbinot1  36164  notbinot2  36168  truconj  36186  sbccom2lem  36209  sbccom2  36210  sbccom2f  36211  tsim1  36215  tsxo3  36224  tsxo4  36225  trcoss2  36529  dfmember3  36713  eqvreldmqs  36714  isopos  37121  islvol5  37520  elpadd0  37750  dvhopellsm  39058  diblsmopel  39112  mapdvalc  39570  3factsumint2  39958  3factsumint3  39959  3factsumint4  39960  aks4d1p1p2  40006  aks4d1p7  40019  sticksstones22  40052  elpwbi  40131  dffltz  40387  rmxypairf1o  40649  ifpnotnotb  40984  ifpdfxor  40992  ifpidg  40996  ifpim123g  41005  ifpim1g  41006  ifpimimb  41009  ifpimim  41014  rp-fakeanorass  41018  elmapintrab  41073  undmrnresiss  41101  clcnvlem  41120  sqrtcvallem1  41128  cnviun  41147  dfxor4  41263  dfhe3  41272  dffrege69  41429  dffrege76  41436  or3or  41520  uneqsn  41522  scottabf  41747  mnurndlem1  41788  ismnushort  41808  pm10.252  41868  pm10.253  41869  pm10.42  41871  aaanv  41895  pm13.195  41920  pm13.196a  41921  sbc3or  42041  en3lpVD  42354  3orbi123VD  42359  sbc3orgVD  42360  sbcoreleleqVD  42368  undif3VD  42391  ax6e2ndeqVD  42418  ax6e2ndeqALT  42440  sineq0ALT  42446  uzwo4  42490  fompt  42619  allbutfiinf  42850  limsupequzmptlem  43159  cncfshift  43305  dvnmul  43374  dvnprodlem2  43378  rrxsnicc  43731  salexct  43763  sge00  43804  sge0iunmpt  43846  meadjiun  43894  carageneld  43930  ovncvrrp  43992  ovolval4lem1  44077  vonioo  44110  vonicc  44113  nsssmfmbf  44201  smfmullem4  44215  aibandbiaiffaiffb  44276  plcofph  44326  pldofph  44327  plvcofph  44328  plvcofphax  44329  plvofpos  44330  fsetsniunop  44430  2reu8i  44492  aovov0bi  44575  tz6.12-afv2  44619  4an21  44649  ichbi12i  44800  ichnfimlem  44803  spr0nelg  44816  sprvalpwn0  44823  reuprpr  44863  requad2  44963  copisnmnd  45251  pgrpgt2nabl  45590  lindslinindsimp2lem5  45691  islininds2  45713  ldepslinc  45738  line2ylem  45985