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  843  pm4.64  849  pm4.25  905  pm4.77  964  pm4.53  987  pm4.55  989  pm4.56  990  pm4.57  992  pm5.63  1021  3anor  1107  3oran  1108  syl3anbr  1161  3an6  1445  nanbi  1496  nornot  1527  truan  1547  truimfal  1560  nottru  1563  falbitru  1566  nic-dfim  1665  nic-dfneg  1666  2nalexn  1824  2nexaln  1826  equvinv  2025  cleljust  2114  sbelx  2250  sb6rfv  2357  cleljustALT  2364  cleljustALT2  2365  dvelimf  2450  sb5rf  2469  sb6rf  2470  sb10f  2529  nexmo  2538  exists2  2659  cleljustab  2714  eqabdv  2872  eqabcri  2883  nne  2941  necon3bbii  2985  necon2abii  2988  necon2bbii  2989  nnel  3053  r19.41v  3186  r3ex  3195  nelbOLD  3232  r19.41  3260  ralcom4OLD  3284  rspc2gv  3631  ceqsrexbv  3655  rabeqcOLD  3692  2reu5lem1  3763  2reu5lem2  3764  2reu5lem3  3765  dfsbcq2  3793  cbvreucsf  3954  nss  4059  dfdif3OLD  4127  symdifass  4267  indifdi  4299  difab  4315  neq0  4357  un0  4399  in0  4400  ss0b  4406  eq0rdv  4412  2nreu  4449  ralidm  4517  ralf0  4519  reuprg  4707  snssb  4786  snssg  4787  ssunsn2  4831  iindif2  5081  eqsnuniex  5366  nssss  5465  snopeqop  5515  dffr6  5643  epse  5670  rnep  5939  cotrgOLDOLD  6131  mptpreima  6259  ralrnmpt  7115  fmptsng  7187  fmptsnd  7188  dff14a  7289  f13dfv  7293  weniso  7373  abnex  7775  uniuni  7780  frpoins3xp3g  8164  xpord3inddlem  8177  eroveu  8850  fsetexb  8902  mapsnend  9074  isfinite2  9331  marypha1lem  9470  marypha2lem4  9475  infcllem  9524  en3lplem2  9650  cantnfp1  9718  carden2  10024  fseqenlem1  10061  iscard3  10130  cardnum  10131  alephinit  10132  cardinfima  10134  alephiso  10135  dfac10b  10177  dfackm  10204  isfin5-2  10428  brdom7disj  10568  brdom6disj  10569  fsuppmapnn0fiubex  14029  hash2prb  14507  hashle2prv  14513  hashtpg  14520  hash3tpb  14530  swrdnnn0nd  14690  wrd2ind  14757  cshwsexaOLD  14859  s4f1o  14953  cotr2g  15011  relexpindlem  15098  lcmfunsnlem2  16673  ncoprmlnprm  16761  vdwapun  17007  cshwsiun  17133  cshwshash  17138  grpss  18984  symgsubmefmnd  19430  pmtrfrn  19490  pmtrrn2  19492  pmtrprfvalrn  19520  issrg  20205  0ringnnzr  20541  acsfn1p  20816  unocv  21715  dsmmacl  21778  pmatcollpw2lem  22798  fvmptnn04if  22870  toptopon  22938  ordtbas2  23214  ordtrest2  23227  xmeterval  24457  isclmp  25143  ovolfcl  25514  eldv  25947  eltayl  26415  musumsum  27249  2sqreu  27514  2sqreunn  27515  2sqreult  27516  2sqreultb  27517  2sqreunnlt  27518  2sqreunnltb  27519  nosupinfsep  27791  umgrislfupgrlem  29153  numedglnl  29175  ausgrusgrb  29196  cplgr3v  29466  vtxd0nedgb  29520  finsumvtxdg2ssteplem1  29577  isrgr  29591  rgrusgrprc  29621  rgrprcx  29624  upgr2wlk  29700  wwlksnwwlksnon  29944  usgr2wspthon  29994  isclwwlk  30012  clwwlkvbij  30141  iseupthf1o  30230  frcond2  30295  nfrgr2v  30300  4cycl2vnunb  30318  fusgr2wsp2nb  30362  frgrregord013  30423  lejdii  31566  mdslle1i  32345  mdslle2i  32346  mdslj1i  32347  mdslj2i  32348  mo5f  32516  n0nsnel  32542  unipreima  32659  2ndpreima  32722  mgccnv  32973  quslsm  33412  ordtrest2NEW  33883  ordtconnlem1  33884  ballotlem2  34469  plymulx0  34540  bnj115  34717  bnj156  34720  bnj206  34723  bnj110  34850  bnj121  34862  bnj124  34863  bnj130  34866  bnj153  34872  bnj207  34873  bnj581  34900  bnj611  34910  bnj864  34914  bnj865  34915  bnj893  34920  bnj1000  34933  bnj978  34941  bnj1040  34964  bnj1049  34966  bnj1133  34981  bnj1189  35001  satfv1  35347  satfvsucsuc  35349  satfdm  35353  satf0  35356  satf0op  35361  fmlafvel  35369  cnvco1  35738  cnvco2  35739  dfiota3  35904  ss-ax8  36207  trer  36298  nabi1i  36376  nabi2i  36377  bj-hbext  36692  bj-nnfbit  36734  bj-dvelimdv  36833  bj-gabima  36922  bj-elsngl  36950  bj-nuliotaALT  37040  bj-rest10  37070  bj-restuni  37079  con1bii2  37314  con2bii2  37315  topdifinfeq  37332  isbasisrelowllem2  37338  wl-1xor  37464  wl-1mintru1  37470  wl-sb8eut  37558  wl-sb8eutv  37559  inixp  37714  notbinot1  38065  notbinot2  38069  truconj  38087  sbccom2lem  38110  sbccom2  38111  sbccom2f  38112  tsim1  38116  tsxo3  38125  tsxo4  38126  trcoss2  38465  dfcomember3  38655  eqvreldmqs  38656  eqvreldmqs2  38657  dfmembpart2  38751  eldisjn0el  38787  isopos  39161  islvol5  39561  elpadd0  39791  dvhopellsm  41099  diblsmopel  41153  mapdvalc  41611  3factsumint2  42003  3factsumint3  42004  3factsumint4  42005  aks4d1p1p2  42051  aks4d1p7  42064  isprimroot  42074  aks6d1c1p1  42088  aks6d1c2p2  42100  sticksstones22  42149  unitscyglem4  42179  elpwbi  42247  redvmptabs  42368  dffltz  42620  rmxypairf1o  42899  onsupmaxb  43227  ifpnotnotb  43468  ifpdfxor  43476  ifpidg  43480  ifpim123g  43489  ifpim1g  43490  ifpimimb  43493  ifpimim  43498  rp-fakeanorass  43502  elmapintrab  43565  undmrnresiss  43593  clcnvlem  43612  sqrtcvallem1  43620  cnviun  43639  dfxor4  43755  dfhe3  43764  dffrege69  43921  dffrege76  43928  or3or  44012  uneqsn  44014  scottabf  44235  mnurndlem1  44276  ismnushort  44296  pm10.252  44356  pm10.253  44357  pm10.42  44359  aaanv  44383  pm13.195  44408  pm13.196a  44409  sbc3or  44529  en3lpVD  44842  3orbi123VD  44847  sbc3orgVD  44848  sbcoreleleqVD  44856  undif3VD  44879  ax6e2ndeqVD  44906  ax6e2ndeqALT  44928  sineq0ALT  44934  uzwo4  44992  iindif2f  45102  allbutfiinf  45369  limsupequzmptlem  45683  cncfshift  45829  dvnmul  45898  dvnprodlem2  45902  rrxsnicc  46255  salexct  46289  sge00  46331  sge0iunmpt  46373  meadjiun  46421  carageneld  46457  ovncvrrp  46519  ovolval4lem1  46604  vonioo  46637  vonicc  46640  nsssmfmbf  46734  smfmullem4  46749  aibandbiaiffaiffb  46843  plcofph  46893  pldofph  46894  plvcofph  46895  plvcofphax  46896  plvofpos  46897  n0nsn2el  46974  fsetsniunop  46998  2reu8i  47062  aovov0bi  47145  tz6.12-afv2  47189  4an21  47219  ichbi12i  47384  ichnfimlem  47387  spr0nelg  47400  sprvalpwn0  47407  reuprpr  47447  requad2  47547  clnbgrel  47752  usgrexmpl2nb4  47929  copisnmnd  48012  pgrpgt2nabl  48210  lindslinindsimp2lem5  48307  islininds2  48329  ldepslinc  48354  line2ylem  48600