Theorem bicomi 226

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

Syntax hints:   ↔ wb 208

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 209

This theorem is referenced by:  biimpri  230  bitr2i  278  bitr3i  279  bitr4i  280  bitr3id  287  bitr3di  288  bitr4di  291  bitr4id  292  mtbir  325  sylnibr  331  sylnbir  333  xchnxbir  335  xchbinxr  337  con1bii  358  nbn  374  xor3  384  pm5.41  392  pm4.63  399  pm4.61  406  pm4.76  524  anidm  570  an21  651  an43  665  anabs1  669  anabs7  671  pm4.87  850  pm4.64  856  pm4.25  912  pm4.77  971  pm4.53  994  pm4.55  996  pm4.56  997  pm4.57  999  pm5.63  1028  3anor  1114  3oran  1115  syl3anbr  1169  3an6  1455  nanbi  1508  nornot  1539  truan  1559  truimfal  1572  nottru  1575  falbitru  1578  nic-dfim  1677  nic-dfneg  1678  2nalexn  1836  2nexaln  1838  equvinv  2037  cleljust  2130  sbelx  2267  sb6rfv  2367  cleljustALT  2374  cleljustALT2  2375  dvelimf  2458  sb5rf  2477  sb6rf  2478  sb10f  2537  nexmo  2547  exists2  2667  cleljustab  2722  eqabdv  2874  eqabcri  2884  nne  2940  necon3bbii  2983  necon2abii  2986  necon2bbii  2987  nnel  3050  r19.41v  3171  r3ex  3180  r19.41  3245  rspc2gv  3571  ceqsrexbv  3595  2reu5lem1  3697  2reu5lem2  3698  2reu5lem3  3699  dfsbcq2  3727  cbvreucsf  3876  nss  3980  dfdif3OLD  4051  symdifass  4192  indifdi  4224  difab  4240  neq0  4282  un0  4324  in0  4325  ss0b  4331  2nreu  4374  ralidm  4447  reuprg  4637  snssb  4716  snssg  4717  ssunsn2  4760  iindif2  5008  eqsnuniex  5292  nssss  5396  snopeqop  5449  dffr6  5576  epse  5602  rnep  5875  mptpreima  6192  ralrnmpt  7040  fmptsng  7115  fmptsnd  7116  dff14a  7217  f13dfv  7221  weniso  7301  abnex  7703  uniuni  7708  frpoins3xp3g  8083  xpord3inddlem  8096  eroveu  8753  fsetexb  8805  mapsnend  8977  isfinite2  9202  marypha1lem  9340  marypha2lem4  9345  infcllem  9395  en3lplem2  9529  cantnfp1  9597  carden2  9906  fseqenlem1  9941  iscard3  10010  cardnum  10011  alephinit  10012  cardinfima  10014  alephiso  10015  dfac10b  10057  dfackm  10084  isfin5-2  10309  brdom7disj  10449  brdom6disj  10450  fsuppmapnn0fiubex  13949  hash2prb  14429  hashle2prv  14435  hashtpg  14442  hash3tpb  14452  swrdnnn0nd  14614  wrd2ind  14680  s4f1o  14875  cotr2g  14933  relexpindlem  15020  lcmfunsnlem2  16604  ncoprmlnprm  16693  vdwapun  16940  cshwsiun  17065  cshwshash  17070  grpss  18925  symgsubmefmnd  19367  pmtrfrn  19427  pmtrrn2  19429  pmtrprfvalrn  19457  issrg  20163  0ringnnzr  20500  acsfn1p  20774  unocv  21658  dsmmacl  21719  pmatcollpw2lem  22763  fvmptnn04if  22835  toptopon  22903  ordtbas2  23177  ordtrest2  23190  xmeterval  24418  isclmp  25085  ovolfcl  25454  eldv  25886  eltayl  26346  musumsum  27176  2sqreu  27440  2sqreunn  27441  2sqreult  27442  2sqreultb  27443  2sqreunnlt  27444  2sqreunnltb  27445  nosupinfsep  27716  umgrislfupgrlem  29211  numedglnl  29233  ausgrusgrb  29254  cplgr3v  29524  vtxd0nedgb  29577  finsumvtxdg2ssteplem1  29634  isrgr  29648  rgrusgrprc  29678  rgrprcx  29681  upgr2wlk  29755  dfpth2  29817  wwlksnwwlksnon  30003  usgr2wspthon  30056  isclwwlk  30074  clwwlkvbij  30203  iseupthf1o  30292  frcond2  30357  nfrgr2v  30362  4cycl2vnunb  30380  fusgr2wsp2nb  30424  frgrregord013  30485  lejdii  31629  mdslle1i  32408  mdslle2i  32409  mdslj1i  32410  mdslj2i  32411  mo5f  32578  n0nsnel  32605  unipreima  32737  2ndpreima  32802  mgccnv  33080  domnprodeq0  33359  quslsm  33490  mplmonprod  33748  ordtrest2NEW  34117  ordtconnlem1  34118  ballotlem2  34683  plymulx0  34741  bnj115  34921  bnj156  34924  bnj206  34927  bnj110  35053  bnj121  35065  bnj124  35066  bnj130  35069  bnj153  35075  bnj207  35076  bnj581  35103  bnj611  35113  bnj864  35117  bnj865  35118  bnj893  35123  bnj1000  35136  bnj978  35144  bnj1040  35167  bnj1049  35169  bnj1133  35184  bnj1189  35204  satfv1  35604  satfvsucsuc  35606  satfdm  35610  satf0  35613  satf0op  35618  fmlafvel  35626  cnvco1  36000  cnvco2  36001  dfiota3  36162  ss-ax8  36466  trer  36557  nabi1i  36635  nabi2i  36636  regsfromregtco  36779  bj-nnfbit  37114  bj-dvelimdv  37217  bj-gabima  37306  bj-elsngl  37334  bj-nuliotaALT  37424  bj-axseprep  37440  bj-rest10  37459  bj-restuni  37468  con1bii2  37707  con2bii2  37708  topdifinfeq  37725  isbasisrelowllem2  37731  wl-1xor  37857  wl-1mintru1  37863  wl-sb8eut  37962  wl-sb8eutv  37963  inixp  38108  notbinot1  38459  notbinot2  38463  truconj  38481  sbccom2lem  38504  sbccom2  38505  sbccom2f  38506  tsim1  38510  tsxo3  38519  tsxo4  38520  trcoss2  38954  dfcomember3  39139  eqvreldmqs  39140  eqvreldmqs2  39141  dfmembpart2  39253  eldisjn0el  39289  isopos  39685  islvol5  40084  elpadd0  40314  dvhopellsm  41622  diblsmopel  41676  mapdvalc  42134  3factsumint2  42520  3factsumint3  42521  3factsumint4  42522  aks4d1p1p2  42568  aks4d1p7  42581  isprimroot  42591  aks6d1c1p1  42605  aks6d1c2p2  42617  sticksstones22  42666  unitscyglem4  42696  elpwbi  42730  redvmptabs  42850  dffltz  43097  rmxypairf1o  43369  onsupmaxb  43697  ifpnotnotb  43936  ifpdfxor  43944  ifpidg  43948  ifpim123g  43957  ifpim1g  43958  ifpimimb  43961  ifpimim  43966  rp-fakeanorass  43970  elmapintrab  44033  undmrnresiss  44061  clcnvlem  44080  sqrtcvallem1  44088  cnviun  44107  dfxor4  44223  dfhe3  44232  dffrege69  44389  dffrege76  44396  or3or  44480  uneqsn  44482  scottabf  44697  mnurndlem1  44738  ismnushort  44758  pm10.252  44818  pm10.253  44819  pm10.42  44821  aaanv  44845  pm13.195  44870  pm13.196a  44871  sbc3or  44989  en3lpVD  45301  3orbi123VD  45306  sbc3orgVD  45307  sbcoreleleqVD  45315  undif3VD  45338  ax6e2ndeqVD  45365  ax6e2ndeqALT  45387  sineq0ALT  45393  n0abso  45433  permaxsep  45464  permaxinf2lem  45469  iindif2f  45619  allbutfiinf  45875  limsupequzmptlem  46183  cncfshift  46329  dvnmul  46398  dvnprodlem2  46402  rrxsnicc  46755  sge00  46831  sge0iunmpt  46873  meadjiun  46921  ovolval4lem1  47104  nsssmfmbf  47234  smfmullem4  47249  aibandbiaiffaiffb  47369  plcofph  47419  pldofph  47420  plvcofph  47421  plvcofphax  47422  plvofpos  47423  n0nsn2el  47500  fsetsniunop  47524  2reu8i  47588  aovov0bi  47671  tz6.12-afv2  47715  4an21  47745  ichbi12i  47947  ichnfimlem  47950  spr0nelg  47963  sprvalpwn0  47970  reuprpr  48010  nprmmul1  48014  requad2  48126  clnbgrel  48331  usgrexmpl2nb4  48538  pg4cyclnex  48630  copisnmnd  48672  pgrpgt2nabl  48869  lindslinindsimp2lem5  48965  islininds2  48987  ldepslinc  49012  line2ylem  49254