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  643  an43  657  anabs1  661  anabs7  663  pm4.87  842  pm4.64  848  pm4.25  904  pm4.77  963  pm4.53  986  pm4.55  988  pm4.56  989  pm4.57  991  pm5.63  1020  3anor  1108  3oran  1109  syl3anbr  1162  3an6  1446  nanbi  1497  nornot  1528  truan  1548  truimfal  1561  nottru  1564  falbitru  1567  nic-dfim  1667  nic-dfneg  1668  2nalexn  1826  2nexaln  1828  equvinv  2028  cleljust  2117  sbelx  2254  sb5OLD  2278  sb6rfv  2363  cleljustALT  2370  cleljustALT2  2371  dvelimf  2456  sb5rf  2475  sb6rf  2476  sb10f  2535  nexmo  2544  exists2  2665  cleljustab  2720  eqabdv  2878  eqabcri  2889  nfabdwOLD  2933  nne  2950  necon3bbii  2994  necon2abii  2997  necon2bbii  2998  nnel  3062  r19.41v  3195  r3ex  3204  nelbOLD  3241  r19.41  3269  ralcom4OLD  3293  rspc2gv  3645  ceqsrexbv  3669  rabeqcOLD  3706  2reu5lem1  3777  2reu5lem2  3778  2reu5lem3  3779  dfsbcq2  3807  cbvreucsf  3968  nss  4073  dfdif3OLD  4141  symdifass  4281  indifdi  4313  difab  4329  neq0  4375  ab0OLD  4403  un0  4417  in0  4418  ss0b  4424  eq0rdv  4430  2nreu  4467  ralidm  4535  ralf0  4537  reuprg  4728  snssb  4807  snssg  4808  ssunsn2  4852  iindif2  5100  eqsnuniex  5379  nssss  5475  snopeqop  5525  dffr6  5655  epse  5682  rnep  5951  cotrgOLDOLD  6141  mptpreima  6269  ralrnmpt  7130  fmptsng  7202  fmptsnd  7203  dff14a  7307  f13dfv  7310  weniso  7390  abnex  7792  uniuni  7797  frpoins3xp3g  8182  xpord3inddlem  8195  eroveu  8870  fsetexb  8922  mapsnend  9101  isfinite2  9362  marypha1lem  9502  marypha2lem4  9507  infcllem  9556  en3lplem2  9682  cantnfp1  9750  carden2  10056  fseqenlem1  10093  iscard3  10162  cardnum  10163  alephinit  10164  cardinfima  10166  alephiso  10167  dfac10b  10209  dfackm  10236  isfin5-2  10460  brdom7disj  10600  brdom6disj  10601  fsuppmapnn0fiubex  14043  hash2prb  14521  hashle2prv  14527  hashtpg  14534  hash3tpb  14544  swrdnnn0nd  14704  wrd2ind  14771  cshwsexaOLD  14873  s4f1o  14967  cotr2g  15025  relexpindlem  15112  lcmfunsnlem2  16687  ncoprmlnprm  16775  vdwapun  17021  cshwsiun  17147  cshwshash  17152  grpss  18994  symgsubmefmnd  19440  pmtrfrn  19500  pmtrrn2  19502  pmtrprfvalrn  19530  issrg  20215  0ringnnzr  20551  acsfn1p  20822  unocv  21721  dsmmacl  21784  pmatcollpw2lem  22804  fvmptnn04if  22876  toptopon  22944  ordtbas2  23220  ordtrest2  23233  xmeterval  24463  isclmp  25149  ovolfcl  25520  eldv  25953  eltayl  26419  musumsum  27253  2sqreu  27518  2sqreunn  27519  2sqreult  27520  2sqreultb  27521  2sqreunnlt  27522  2sqreunnltb  27523  nosupinfsep  27795  umgrislfupgrlem  29157  numedglnl  29179  ausgrusgrb  29200  cplgr3v  29470  vtxd0nedgb  29524  finsumvtxdg2ssteplem1  29581  isrgr  29595  rgrusgrprc  29625  rgrprcx  29628  upgr2wlk  29704  wwlksnwwlksnon  29948  usgr2wspthon  29998  isclwwlk  30016  clwwlkvbij  30145  iseupthf1o  30234  frcond2  30299  nfrgr2v  30304  4cycl2vnunb  30322  fusgr2wsp2nb  30366  frgrregord013  30427  lejdii  31570  mdslle1i  32349  mdslle2i  32350  mdslj1i  32351  mdslj2i  32352  mo5f  32517  n0nsnel  32544  unipreima  32662  2ndpreima  32719  mgccnv  32972  quslsm  33398  ordtrest2NEW  33869  ordtconnlem1  33870  ballotlem2  34453  plymulx0  34524  bnj115  34701  bnj156  34704  bnj206  34707  bnj110  34834  bnj121  34846  bnj124  34847  bnj130  34850  bnj153  34856  bnj207  34857  bnj581  34884  bnj611  34894  bnj864  34898  bnj865  34899  bnj893  34904  bnj1000  34917  bnj978  34925  bnj1040  34948  bnj1049  34950  bnj1133  34965  bnj1189  34985  satfv1  35331  satfvsucsuc  35333  satfdm  35337  satf0  35340  satf0op  35345  fmlafvel  35353  cnvco1  35721  cnvco2  35722  dfiota3  35887  ss-ax8  36191  trer  36282  nabi1i  36360  nabi2i  36361  bj-hbext  36676  bj-nnfbit  36718  bj-dvelimdv  36817  bj-gabima  36906  bj-elsngl  36934  bj-nuliotaALT  37024  bj-rest10  37054  bj-restuni  37063  con1bii2  37298  con2bii2  37299  topdifinfeq  37316  isbasisrelowllem2  37322  wl-1xor  37448  wl-1mintru1  37454  wl-sb8eut  37532  wl-sb8eutv  37533  inixp  37688  notbinot1  38039  notbinot2  38043  truconj  38061  sbccom2lem  38084  sbccom2  38085  sbccom2f  38086  tsim1  38090  tsxo3  38099  tsxo4  38100  trcoss2  38440  dfcomember3  38630  eqvreldmqs  38631  eqvreldmqs2  38632  dfmembpart2  38726  eldisjn0el  38762  isopos  39136  islvol5  39536  elpadd0  39766  dvhopellsm  41074  diblsmopel  41128  mapdvalc  41586  3factsumint2  41979  3factsumint3  41980  3factsumint4  41981  aks4d1p1p2  42027  aks4d1p7  42040  isprimroot  42050  aks6d1c1p1  42064  aks6d1c2p2  42076  sticksstones22  42125  unitscyglem4  42155  elpwbi  42223  dffltz  42589  rmxypairf1o  42868  onsupmaxb  43200  ifpnotnotb  43441  ifpdfxor  43449  ifpidg  43453  ifpim123g  43462  ifpim1g  43463  ifpimimb  43466  ifpimim  43471  rp-fakeanorass  43475  elmapintrab  43538  undmrnresiss  43566  clcnvlem  43585  sqrtcvallem1  43593  cnviun  43612  dfxor4  43728  dfhe3  43737  dffrege69  43894  dffrege76  43901  or3or  43985  uneqsn  43987  scottabf  44209  mnurndlem1  44250  ismnushort  44270  pm10.252  44330  pm10.253  44331  pm10.42  44333  aaanv  44357  pm13.195  44382  pm13.196a  44383  sbc3or  44503  en3lpVD  44816  3orbi123VD  44821  sbc3orgVD  44822  sbcoreleleqVD  44830  undif3VD  44853  ax6e2ndeqVD  44880  ax6e2ndeqALT  44902  sineq0ALT  44908  uzwo4  44955  iindif2f  45065  allbutfiinf  45335  limsupequzmptlem  45649  cncfshift  45795  dvnmul  45864  dvnprodlem2  45868  rrxsnicc  46221  salexct  46255  sge00  46297  sge0iunmpt  46339  meadjiun  46387  carageneld  46423  ovncvrrp  46485  ovolval4lem1  46570  vonioo  46603  vonicc  46606  nsssmfmbf  46700  smfmullem4  46715  aibandbiaiffaiffb  46809  plcofph  46859  pldofph  46860  plvcofph  46861  plvcofphax  46862  plvofpos  46863  n0nsn2el  46940  fsetsniunop  46964  2reu8i  47028  aovov0bi  47111  tz6.12-afv2  47155  4an21  47185  ichbi12i  47334  ichnfimlem  47337  spr0nelg  47350  sprvalpwn0  47357  reuprpr  47397  requad2  47497  clnbgrel  47701  usgrexmpl2nb4  47850  copisnmnd  47892  pgrpgt2nabl  48091  lindslinindsimp2lem5  48191  islininds2  48213  ldepslinc  48238  line2ylem  48485