Theorem bicomi 224

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

Syntax hints:   ↔ wb 206

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 207

This theorem is referenced by:  biimpri  228  bitr2i  276  bitr3i  277  bitr4i  278  bitr3id  285  bitr3di  286  bitr4di  289  bitr4id  290  mtbir  323  sylnibr  329  sylnbir  331  xchnxbir  333  xchbinxr  335  con1bii  356  nbn  372  xor3  382  pm5.41  390  pm4.63  397  pm4.61  404  pm4.76  518  anidm  564  an21  644  an43  658  anabs1  662  anabs7  664  pm4.87  844  pm4.64  850  pm4.25  906  pm4.77  965  pm4.53  988  pm4.55  990  pm4.56  991  pm4.57  993  pm5.63  1022  3anor  1108  3oran  1109  syl3anbr  1163  3an6  1448  nanbi  1500  nornot  1531  truan  1551  truimfal  1564  nottru  1567  falbitru  1570  nic-dfim  1669  nic-dfneg  1670  2nalexn  1828  2nexaln  1830  equvinv  2028  cleljust  2117  sbelx  2253  sb6rfv  2360  cleljustALT  2367  cleljustALT2  2368  dvelimf  2453  sb5rf  2472  sb6rf  2473  sb10f  2532  nexmo  2541  exists2  2662  cleljustab  2717  eqabdv  2875  eqabcri  2886  nne  2944  necon3bbii  2988  necon2abii  2991  necon2bbii  2992  nnel  3056  r19.41v  3189  r3ex  3198  nelbOLD  3235  r19.41  3263  ralcom4OLD  3287  rspc2gv  3632  ceqsrexbv  3656  rabeqcOLD  3690  2reu5lem1  3761  2reu5lem2  3762  2reu5lem3  3763  dfsbcq2  3791  cbvreucsf  3943  nss  4048  dfdif3OLD  4118  symdifass  4262  indifdi  4294  difab  4310  neq0  4352  un0  4394  in0  4395  ss0b  4401  eq0rdv  4407  2nreu  4444  ralidm  4512  ralf0  4514  reuprg  4703  snssb  4782  snssg  4783  ssunsn2  4827  iindif2  5077  eqsnuniex  5361  nssss  5460  snopeqop  5511  dffr6  5640  epse  5667  rnep  5937  cotrgOLDOLD  6129  mptpreima  6258  ralrnmpt  7116  fmptsng  7188  fmptsnd  7189  dff14a  7290  f13dfv  7294  weniso  7374  abnex  7777  uniuni  7782  frpoins3xp3g  8166  xpord3inddlem  8179  eroveu  8852  fsetexb  8904  mapsnend  9076  isfinite2  9334  marypha1lem  9473  marypha2lem4  9478  infcllem  9527  en3lplem2  9653  cantnfp1  9721  carden2  10027  fseqenlem1  10064  iscard3  10133  cardnum  10134  alephinit  10135  cardinfima  10137  alephiso  10138  dfac10b  10180  dfackm  10207  isfin5-2  10431  brdom7disj  10571  brdom6disj  10572  fsuppmapnn0fiubex  14033  hash2prb  14511  hashle2prv  14517  hashtpg  14524  hash3tpb  14534  swrdnnn0nd  14694  wrd2ind  14761  cshwsexaOLD  14863  s4f1o  14957  cotr2g  15015  relexpindlem  15102  lcmfunsnlem2  16677  ncoprmlnprm  16765  vdwapun  17012  cshwsiun  17137  cshwshash  17142  grpss  18972  symgsubmefmnd  19416  pmtrfrn  19476  pmtrrn2  19478  pmtrprfvalrn  19506  issrg  20185  0ringnnzr  20525  acsfn1p  20800  unocv  21698  dsmmacl  21761  pmatcollpw2lem  22783  fvmptnn04if  22855  toptopon  22923  ordtbas2  23199  ordtrest2  23212  xmeterval  24442  isclmp  25130  ovolfcl  25501  eldv  25933  eltayl  26401  musumsum  27235  2sqreu  27500  2sqreunn  27501  2sqreult  27502  2sqreultb  27503  2sqreunnlt  27504  2sqreunnltb  27505  nosupinfsep  27777  umgrislfupgrlem  29139  numedglnl  29161  ausgrusgrb  29182  cplgr3v  29452  vtxd0nedgb  29506  finsumvtxdg2ssteplem1  29563  isrgr  29577  rgrusgrprc  29607  rgrprcx  29610  upgr2wlk  29686  dfpth2  29749  wwlksnwwlksnon  29935  usgr2wspthon  29985  isclwwlk  30003  clwwlkvbij  30132  iseupthf1o  30221  frcond2  30286  nfrgr2v  30291  4cycl2vnunb  30309  fusgr2wsp2nb  30353  frgrregord013  30414  lejdii  31557  mdslle1i  32336  mdslle2i  32337  mdslj1i  32338  mdslj2i  32339  mo5f  32508  n0nsnel  32534  unipreima  32653  2ndpreima  32717  mgccnv  32989  quslsm  33433  ordtrest2NEW  33922  ordtconnlem1  33923  ballotlem2  34491  plymulx0  34562  bnj115  34739  bnj156  34742  bnj206  34745  bnj110  34872  bnj121  34884  bnj124  34885  bnj130  34888  bnj153  34894  bnj207  34895  bnj581  34922  bnj611  34932  bnj864  34936  bnj865  34937  bnj893  34942  bnj1000  34955  bnj978  34963  bnj1040  34986  bnj1049  34988  bnj1133  35003  bnj1189  35023  satfv1  35368  satfvsucsuc  35370  satfdm  35374  satf0  35377  satf0op  35382  fmlafvel  35390  cnvco1  35759  cnvco2  35760  dfiota3  35924  ss-ax8  36226  trer  36317  nabi1i  36395  nabi2i  36396  bj-hbext  36711  bj-nnfbit  36753  bj-dvelimdv  36852  bj-gabima  36941  bj-elsngl  36969  bj-nuliotaALT  37059  bj-rest10  37089  bj-restuni  37098  con1bii2  37333  con2bii2  37334  topdifinfeq  37351  isbasisrelowllem2  37357  wl-1xor  37483  wl-1mintru1  37489  wl-sb8eut  37579  wl-sb8eutv  37580  inixp  37735  notbinot1  38086  notbinot2  38090  truconj  38108  sbccom2lem  38131  sbccom2  38132  sbccom2f  38133  tsim1  38137  tsxo3  38146  tsxo4  38147  trcoss2  38485  dfcomember3  38675  eqvreldmqs  38676  eqvreldmqs2  38677  dfmembpart2  38771  eldisjn0el  38807  isopos  39181  islvol5  39581  elpadd0  39811  dvhopellsm  41119  diblsmopel  41173  mapdvalc  41631  3factsumint2  42023  3factsumint3  42024  3factsumint4  42025  aks4d1p1p2  42071  aks4d1p7  42084  isprimroot  42094  aks6d1c1p1  42108  aks6d1c2p2  42120  sticksstones22  42169  unitscyglem4  42199  elpwbi  42269  redvmptabs  42390  dffltz  42644  rmxypairf1o  42923  onsupmaxb  43251  ifpnotnotb  43492  ifpdfxor  43500  ifpidg  43504  ifpim123g  43513  ifpim1g  43514  ifpimimb  43517  ifpimim  43522  rp-fakeanorass  43526  elmapintrab  43589  undmrnresiss  43617  clcnvlem  43636  sqrtcvallem1  43644  cnviun  43663  dfxor4  43779  dfhe3  43788  dffrege69  43945  dffrege76  43952  or3or  44036  uneqsn  44038  scottabf  44259  mnurndlem1  44300  ismnushort  44320  pm10.252  44380  pm10.253  44381  pm10.42  44383  aaanv  44407  pm13.195  44432  pm13.196a  44433  sbc3or  44552  en3lpVD  44865  3orbi123VD  44870  sbc3orgVD  44871  sbcoreleleqVD  44879  undif3VD  44902  ax6e2ndeqVD  44929  ax6e2ndeqALT  44951  sineq0ALT  44957  n0abso  44993  uzwo4  45058  iindif2f  45165  allbutfiinf  45431  limsupequzmptlem  45743  cncfshift  45889  dvnmul  45958  dvnprodlem2  45962  rrxsnicc  46315  salexct  46349  sge00  46391  sge0iunmpt  46433  meadjiun  46481  carageneld  46517  ovncvrrp  46579  ovolval4lem1  46664  vonioo  46697  vonicc  46700  nsssmfmbf  46794  smfmullem4  46809  aibandbiaiffaiffb  46906  plcofph  46956  pldofph  46957  plvcofph  46958  plvcofphax  46959  plvofpos  46960  n0nsn2el  47037  fsetsniunop  47061  2reu8i  47125  aovov0bi  47208  tz6.12-afv2  47252  4an21  47282  ichbi12i  47447  ichnfimlem  47450  spr0nelg  47463  sprvalpwn0  47470  reuprpr  47510  requad2  47610  clnbgrel  47815  usgrexmpl2nb4  47994  copisnmnd  48085  pgrpgt2nabl  48282  lindslinindsimp2lem5  48379  islininds2  48401  ldepslinc  48426  line2ylem  48672