Theorem bicomi 227

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

This proof depends on syntax axioms:   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  biimpri  231  bitr2i  279  bitr3i  280  bitr4i  281  bitr3id  288  bitr3di  289  bitr4di  292  bitr4id  293  mtbir  326  sylnibr  332  sylnbir  334  xchnxbir  336  xchbinxr  338  con1bii  359  nbn  375  xor3  385  pm5.41  395  pm4.63  403  pm4.61  410  pm4.76  528  anidm  575  an21  657  an43  671  anabs1  675  anabs7  677  pm4.87  857  pm4.64  863  pm4.25  919  pm4.77  977  pm4.53  1001  pm4.55  1003  pm4.56  1004  pm4.57  1006  pm5.63  1037  3anor  1125  3oran  1126  syl3anbr  1180  3an6  1475  nanbi  1530  nornot  1561  truan  1581  truimfal  1594  nottru  1597  falbitru  1600  had0  1634  nic-dfim  1702  nic-dfneg  1703  2nalexn  1861  2nexaln  1863  equvinv  2062  cleljust  2154  sbelx  2288  sb6rfv  2386  cleljustALT  2393  cleljustALT2  2394  dvelimf  2477  sb5rf  2496  sb6rf  2497  sb10f  2556  nexmo  2566  exists2  2686  cleljustab  2741  eqabdv  2893  eqabcri  2903  nne  2959  necon3bbii  3002  necon2abii  3005  necon2bbii  3006  nnel  3071  r19.41v  3192  r3ex  3201  r19.41  3266  rspc2gv  3586  ceqsrexbv  3610  2reu5lem1  3713  2reu5lem2  3714  2reu5lem3  3715  dfsbcq2  3742  cbvreucsf  3891  nss  3995  symdifass  4208  indifdi  4240  difab  4256  neq0  4299  un0  4344  in0  4345  ss0b  4351  2nreu  4402  ralidm  4473  reuprg  4664  snssb  4743  snssg  4744  ssunsn2  4788  iindif2  5037  eqsnuniex  5326  nssss  5430  snopeqop  5483  dffr6  5611  epse  5637  rnep  5913  mptpreima  6236  ralrnmpt  7092  fmptsng  7169  fmptsnd  7170  dff14a  7270  f13dfv  7278  weniso  7360  abnex  7762  uniuni  7767  frpoins3xp3g  8144  xpord3inddlem  8157  eroveu  8819  fsetexb  8872  mapsnend  9050  isfinite2  9275  marypha1lem  9410  marypha2lem4  9415  infcllem  9465  en3lplem2  9599  cantnfp1  9667  scottabf  9903  carden2  10017  fseqenlem1  10052  iscard3  10121  cardnum  10122  alephinit  10123  cardinfima  10125  alephiso  10126  dfac10b  10167  dfackm  10194  isfin5-2  10418  brdom7disj  10559  brdom6disj  10560  fsuppmapnn0fiubex  14081  hash2prb  14562  hashle2prv  14568  hashtpg  14575  hash3tpb  14585  swrdnnn0nd  14751  wrd2ind  14817  s4f1o  15014  cotr2g  15074  relexpindlem  15161  lcmfunsnlem2  16755  ncoprmlnprm  16844  vdwapun  17091  cshwsiun  17216  cshwshash  17221  degenmgm2nfun  19078  grpss  19104  symgsubmefmnd  19551  pmtrfrn  19611  pmtrrn2  19613  pmtrprfvalrn  19641  issrg  20353  dfring3  20457  0ringnnzr  20715  acsfn1p  20995  unocv  21925  dsmmacl  21986  pmatcollpw2lem  23034  fvmptnn04if  23106  toptopon  23174  ordtbas2  23448  ordtrest2  23461  xmeterval  24690  isclmp  25357  ovolfcl  25726  eldv  26157  plyn0mulidp  26543  eltayl  26628  musumsum  27460  2sqreu  27724  2sqreunn  27725  2sqreult  27726  2sqreultb  27727  2sqreunnlt  27728  2sqreunnltb  27729  nosupinfsep  28000  umgrislfupgrlem  29611  numedglnl  29633  ausgrusgrb  29657  cplgr3v  29927  vtxd0nedgb  29980  finsumvtxdg2ssteplem1  30037  isrgr  30051  rgrusgrprc  30081  rgrprcx  30084  upgr2wlk  30158  dfpth2  30225  wwlksnwwlksnon  30415  usgr2wspthon  30468  isclwwlk  30486  clwwlkvbij  30615  iseupthf1o  30714  frcond2  30779  nfrgr2v  30784  4cycl2vnunb  30802  fusgr2wsp2nb  30846  frgrregord013  30907  lejdii  32051  mdslle1i  32830  mdslle2i  32831  mdslj1i  32832  mdslj2i  32833  mo5f  32996  n0nsnel  33022  unipreima  33148  2ndpreima  33212  mgccnv  33471  domnprodeq0  33751  quslsm  33867  mplmonprod  34097  ordtrest2NEW  34466  ordtconnlem1  34467  ballotlem2  35033  bnj115  35268  bnj156  35271  bnj206  35274  bnj110  35400  bnj121  35412  bnj124  35413  bnj130  35416  bnj153  35422  bnj207  35423  bnj581  35450  bnj611  35460  bnj864  35464  bnj865  35465  bnj893  35470  bnj1000  35483  bnj978  35491  bnj1040  35514  bnj1049  35516  bnj1133  35531  bnj1189  35551  satfv1  36025  satfvsucsuc  36027  satfdm  36031  satf0  36034  satf0op  36039  fmlafvel  36047  cnvco1  36421  cnvco2  36422  dfiota3  36583  ss-ax8  36912  trer  37002  nabi1i  37080  nabi2i  37081  regsfromregtco  37224  bj-nnfbit  37558  bj-dvelimdv  37661  bj-gabima  37751  bj-elsngl  37779  bj-nuliotaALT  37869  bj-axseprep  37886  bj-rest10  37905  bj-restuni  37914  con1bii2  38151  con2bii2  38152  topdifinfeq  38169  isbasisrelowllem2  38175  wl-1xor  38301  wl-1mintru1  38307  wl-sb8eut  38406  wl-sb8eutv  38407  inixp  38543  notbinot1  38894  notbinot2  38898  truconj  38914  sbccom2lem  38937  sbccom2  38938  sbccom2f  38939  tsim1  38943  tsxo3  38952  tsxo4  38953  trcoss2  39387  dfcomember3  39572  eqvreldmqs  39573  eqvreldmqs2  39574  dfmembpart2  39686  eldisjn0el  39722  isopos  40118  islvol5  40517  elpadd0  40747  dvhopellsm  42055  diblsmopel  42109  mapdvalc  42567  3factsumint2  42953  3factsumint3  42954  3factsumint4  42955  aks4d1p1p2  43001  aks4d1p7  43014  isprimroot  43024  aks6d1c1p1  43038  aks6d1c2p2  43050  sticksstones22  43099  unitscyglem4  43129  elpwbi  43165  redvmptabs  43300  dffltz  43545  rmxypairf1o  43817  onsupmaxb  44145  ifpnotnotb  44384  ifpdfxor  44392  ifpidg  44396  ifpim123g  44405  ifpim1g  44406  ifpimimb  44409  ifpimim  44414  rp-fakeanorass  44418  elmapintrab  44481  undmrnresiss  44509  clcnvlem  44528  sqrtcvallem1  44536  cnviun  44555  dfxor4  44671  dfhe3  44680  dffrege69  44837  dffrege76  44844  or3or  44928  uneqsn  44930  mnurndlem1  45170  ismnushort  45190  pm10.252  45250  pm10.253  45251  pm10.42  45253  aaanv  45277  pm13.195  45302  pm13.196a  45303  sbc3or  45420  en3lpVD  45732  3orbi123VD  45737  sbc3orgVD  45738  sbcoreleleqVD  45746  undif3VD  45769  ax6e2ndeqVD  45796  ax6e2ndeqALT  45818  sineq0ALT  45824  n0abso  45864  permaxsep  45895  permaxinf2lem  45900  iindif2f  46057  allbutfiinf  46313  limsupequzmptlem  46621  cncfshift  46767  dvnmul  46836  dvnprodlem2  46840  rrxsnicc  47193  sge00  47269  sge0iunmpt  47311  meadjiun  47359  ovolval4lem1  47542  nsssmfmbf  47672  smfmullem4  47687  aibandbiaiffaiffb  47847  plcofph  47897  pldofph  47898  plvcofph  47899  plvcofphax  47900  plvofpos  47901  n0nsn2el  47978  fsetsniunop  48002  2reu8i  48066  aovov0bi  48149  tz6.12-afv2  48193  4an21  48223  ichbi12i  48425  ichnfimlem  48428  spr0nelg  48441  sprvalpwn0  48448  reuprpr  48488  nprmmul1  48492  requad2  48604  clnbgrel  48809  usgrexmpl2nb4  49016  pg4cyclnex  49108  copisnmnd  49149  isprmrng  49316  pgrpgt2nabl  49361  lindslinindsimp2lem5  49457  islininds2  49479  ldepslinc  49504  line2ylem  49746  alsanmo  50804  ralsanmo  50805  alsralrex  50806  2alsraln0id  50812