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  645  an43  659  anabs1  663  anabs7  665  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  1449  nanbi  1502  nornot  1533  truan  1553  truimfal  1566  nottru  1569  falbitru  1572  nic-dfim  1671  nic-dfneg  1672  2nalexn  1830  2nexaln  1832  equvinv  2031  cleljust  2123  sbelx  2259  sb6rfv  2360  cleljustALT  2367  cleljustALT2  2368  dvelimf  2451  sb5rf  2470  sb6rf  2471  sb10f  2530  nexmo  2540  exists2  2661  cleljustab  2716  eqabdv  2868  eqabcri  2878  nne  2935  necon3bbii  2978  necon2abii  2981  necon2bbii  2982  nnel  3045  r19.41v  3165  r3ex  3174  r19.41  3239  rspc2gv  3585  ceqsrexbv  3609  2reu5lem1  3712  2reu5lem2  3713  2reu5lem3  3714  dfsbcq2  3742  cbvreucsf  3892  nss  3997  dfdif3OLD  4069  symdifass  4213  indifdi  4245  difab  4261  neq0  4303  un0  4345  in0  4346  ss0b  4352  2nreu  4395  ralidm  4469  reuprg  4659  snssb  4738  snssg  4739  ssunsn2  4782  iindif2  5031  eqsnuniex  5305  nssss  5402  snopeqop  5453  dffr6  5579  epse  5605  rnep  5875  mptpreima  6195  ralrnmpt  7041  fmptsng  7114  fmptsnd  7115  dff14a  7216  f13dfv  7220  weniso  7300  abnex  7702  uniuni  7707  frpoins3xp3g  8083  xpord3inddlem  8096  eroveu  8751  fsetexb  8803  mapsnend  8975  isfinite2  9200  marypha1lem  9338  marypha2lem4  9343  infcllem  9393  en3lplem2  9524  cantnfp1  9592  carden2  9901  fseqenlem1  9936  iscard3  10005  cardnum  10006  alephinit  10007  cardinfima  10009  alephiso  10010  dfac10b  10052  dfackm  10079  isfin5-2  10303  brdom7disj  10443  brdom6disj  10444  fsuppmapnn0fiubex  13917  hash2prb  14397  hashle2prv  14403  hashtpg  14410  hash3tpb  14420  swrdnnn0nd  14582  wrd2ind  14648  s4f1o  14843  cotr2g  14901  relexpindlem  14988  lcmfunsnlem2  16569  ncoprmlnprm  16657  vdwapun  16904  cshwsiun  17029  cshwshash  17034  grpss  18886  symgsubmefmnd  19329  pmtrfrn  19389  pmtrrn2  19391  pmtrprfvalrn  19419  issrg  20125  0ringnnzr  20460  acsfn1p  20734  unocv  21637  dsmmacl  21698  pmatcollpw2lem  22723  fvmptnn04if  22795  toptopon  22863  ordtbas2  23137  ordtrest2  23150  xmeterval  24378  isclmp  25055  ovolfcl  25425  eldv  25857  eltayl  26325  musumsum  27160  2sqreu  27425  2sqreunn  27426  2sqreult  27427  2sqreultb  27428  2sqreunnlt  27429  2sqreunnltb  27430  nosupinfsep  27702  bdayfinbndlem1  28444  umgrislfupgrlem  29176  numedglnl  29198  ausgrusgrb  29219  cplgr3v  29489  vtxd0nedgb  29543  finsumvtxdg2ssteplem1  29600  isrgr  29614  rgrusgrprc  29644  rgrprcx  29647  upgr2wlk  29721  dfpth2  29783  wwlksnwwlksnon  29969  usgr2wspthon  30022  isclwwlk  30040  clwwlkvbij  30169  iseupthf1o  30258  frcond2  30323  nfrgr2v  30328  4cycl2vnunb  30346  fusgr2wsp2nb  30390  frgrregord013  30451  lejdii  31594  mdslle1i  32373  mdslle2i  32374  mdslj1i  32375  mdslj2i  32376  mo5f  32543  n0nsnel  32570  unipreima  32701  2ndpreima  32766  mgccnv  33060  domnprodeq0  33337  quslsm  33465  ordtrest2NEW  34059  ordtconnlem1  34060  ballotlem2  34625  plymulx0  34683  bnj115  34860  bnj156  34863  bnj206  34866  bnj110  34993  bnj121  35005  bnj124  35006  bnj130  35009  bnj153  35015  bnj207  35016  bnj581  35043  bnj611  35053  bnj864  35057  bnj865  35058  bnj893  35063  bnj1000  35076  bnj978  35084  bnj1040  35107  bnj1049  35109  bnj1133  35124  bnj1189  35144  satfv1  35536  satfvsucsuc  35538  satfdm  35542  satf0  35545  satf0op  35550  fmlafvel  35558  cnvco1  35932  cnvco2  35933  dfiota3  36094  ss-ax8  36398  trer  36489  nabi1i  36567  nabi2i  36568  bj-hbext  36884  bj-nnfbit  36926  bj-dvelimdv  37025  bj-gabima  37114  bj-elsngl  37142  bj-nuliotaALT  37232  bj-rest10  37262  bj-restuni  37271  con1bii2  37506  con2bii2  37507  topdifinfeq  37524  isbasisrelowllem2  37530  wl-1xor  37656  wl-1mintru1  37662  wl-sb8eut  37752  wl-sb8eutv  37753  inixp  37898  notbinot1  38249  notbinot2  38253  truconj  38271  sbccom2lem  38294  sbccom2  38295  sbccom2f  38296  tsim1  38300  tsxo3  38309  tsxo4  38310  trcoss2  38744  dfcomember3  38929  eqvreldmqs  38930  eqvreldmqs2  38931  dfmembpart2  39043  eldisjn0el  39079  isopos  39475  islvol5  39874  elpadd0  40104  dvhopellsm  41412  diblsmopel  41466  mapdvalc  41924  3factsumint2  42311  3factsumint3  42312  3factsumint4  42313  aks4d1p1p2  42359  aks4d1p7  42372  isprimroot  42382  aks6d1c1p1  42396  aks6d1c2p2  42408  sticksstones22  42457  unitscyglem4  42487  elpwbi  42524  redvmptabs  42652  dffltz  42914  rmxypairf1o  43190  onsupmaxb  43518  ifpnotnotb  43757  ifpdfxor  43765  ifpidg  43769  ifpim123g  43778  ifpim1g  43779  ifpimimb  43782  ifpimim  43787  rp-fakeanorass  43791  elmapintrab  43854  undmrnresiss  43882  clcnvlem  43901  sqrtcvallem1  43909  cnviun  43928  dfxor4  44044  dfhe3  44053  dffrege69  44210  dffrege76  44217  or3or  44301  uneqsn  44303  scottabf  44518  mnurndlem1  44559  ismnushort  44579  pm10.252  44639  pm10.253  44640  pm10.42  44642  aaanv  44666  pm13.195  44691  pm13.196a  44692  sbc3or  44810  en3lpVD  45122  3orbi123VD  45127  sbc3orgVD  45128  sbcoreleleqVD  45136  undif3VD  45159  ax6e2ndeqVD  45186  ax6e2ndeqALT  45208  sineq0ALT  45214  n0abso  45254  permaxsep  45285  permaxinf2lem  45290  uzwo4  45335  iindif2f  45441  allbutfiinf  45701  limsupequzmptlem  46009  cncfshift  46155  dvnmul  46224  dvnprodlem2  46228  rrxsnicc  46581  salexct  46615  sge00  46657  sge0iunmpt  46699  meadjiun  46747  carageneld  46783  ovncvrrp  46845  ovolval4lem1  46930  vonioo  46963  vonicc  46966  nsssmfmbf  47060  smfmullem4  47075  aibandbiaiffaiffb  47177  plcofph  47227  pldofph  47228  plvcofph  47229  plvcofphax  47230  plvofpos  47231  n0nsn2el  47308  fsetsniunop  47332  2reu8i  47396  aovov0bi  47479  tz6.12-afv2  47523  4an21  47553  ichbi12i  47743  ichnfimlem  47746  spr0nelg  47759  sprvalpwn0  47766  reuprpr  47806  requad2  47906  clnbgrel  48111  usgrexmpl2nb4  48318  pg4cyclnex  48410  copisnmnd  48452  pgrpgt2nabl  48649  lindslinindsimp2lem5  48745  islininds2  48767  ldepslinc  48792  line2ylem  49034