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  2290  sb6rfv  2388  cleljustALT  2395  cleljustALT2  2396  dvelimf  2479  sb5rf  2498  sb6rf  2499  sb10f  2558  nexmo  2568  exists2  2688  cleljustab  2743  eqabdv  2895  eqabcri  2905  nne  2961  necon3bbii  3004  necon2abii  3007  necon2bbii  3008  nnel  3073  r19.41v  3194  r3ex  3203  r19.41  3268  rspc2gv  3589  ceqsrexbv  3613  2reu5lem1  3716  2reu5lem2  3717  2reu5lem3  3718  dfsbcq2  3745  cbvreucsf  3894  nss  3998  symdifass  4211  indifdi  4243  difab  4259  neq0  4302  un0  4347  in0  4348  ss0b  4354  2nreu  4405  ralidm  4476  reuprg  4667  snssb  4746  snssg  4747  ssunsn2  4791  iindif2  5041  eqsnuniex  5330  nssss  5434  snopeqop  5487  dffr6  5615  epse  5641  rnep  5915  mptpreima  6238  ralrnmpt  7092  fmptsng  7169  fmptsnd  7170  dff14a  7270  f13dfv  7278  weniso  7360  abnex  7759  uniuni  7764  frpoins3xp3g  8142  xpord3inddlem  8155  eroveu  8815  fsetexb  8868  mapsnend  9046  isfinite2  9271  marypha1lem  9406  marypha2lem4  9411  infcllem  9461  en3lplem2  9595  cantnfp1  9663  scottabf  9881  carden2  9995  fseqenlem1  10030  iscard3  10099  cardnum  10100  alephinit  10101  cardinfima  10103  alephiso  10104  dfac10b  10145  dfackm  10172  isfin5-2  10396  brdom7disj  10537  brdom6disj  10538  fsuppmapnn0fiubex  14056  hash2prb  14537  hashle2prv  14543  hashtpg  14550  hash3tpb  14560  swrdnnn0nd  14726  wrd2ind  14792  s4f1o  14989  cotr2g  15049  relexpindlem  15136  lcmfunsnlem2  16732  ncoprmlnprm  16821  vdwapun  17068  cshwsiun  17193  cshwshash  17198  degenmgm2nfun  19051  grpss  19077  symgsubmefmnd  19524  pmtrfrn  19584  pmtrrn2  19586  pmtrprfvalrn  19614  issrg  20326  0ringnnzr  20685  acsfn1p  20964  unocv  21892  dsmmacl  21953  pmatcollpw2lem  23001  fvmptnn04if  23073  toptopon  23141  ordtbas2  23415  ordtrest2  23428  xmeterval  24657  isclmp  25324  ovolfcl  25693  eldv  26125  plyn0mulidp  26510  eltayl  26591  musumsum  27424  2sqreu  27688  2sqreunn  27689  2sqreult  27690  2sqreultb  27691  2sqreunnlt  27692  2sqreunnltb  27693  nosupinfsep  27964  umgrislfupgrlem  29563  numedglnl  29585  ausgrusgrb  29609  cplgr3v  29879  vtxd0nedgb  29932  finsumvtxdg2ssteplem1  29989  isrgr  30003  rgrusgrprc  30033  rgrprcx  30036  upgr2wlk  30110  dfpth2  30177  wwlksnwwlksnon  30367  usgr2wspthon  30420  isclwwlk  30438  clwwlkvbij  30567  iseupthf1o  30666  frcond2  30731  nfrgr2v  30736  4cycl2vnunb  30754  fusgr2wsp2nb  30798  frgrregord013  30859  lejdii  32003  mdslle1i  32782  mdslle2i  32783  mdslj1i  32784  mdslj2i  32785  mo5f  32948  n0nsnel  32974  unipreima  33101  2ndpreima  33165  mgccnv  33424  domnprodeq0  33704  quslsm  33819  mplmonprod  34049  ordtrest2NEW  34418  ordtconnlem1  34419  ballotlem2  34985  bnj115  35220  bnj156  35223  bnj206  35226  bnj110  35352  bnj121  35364  bnj124  35365  bnj130  35368  bnj153  35374  bnj207  35375  bnj581  35402  bnj611  35412  bnj864  35416  bnj865  35417  bnj893  35422  bnj1000  35435  bnj978  35443  bnj1040  35466  bnj1049  35468  bnj1133  35483  bnj1189  35503  satfv1  35927  satfvsucsuc  35929  satfdm  35933  satf0  35936  satf0op  35941  fmlafvel  35949  cnvco1  36323  cnvco2  36324  dfiota3  36485  ss-ax8  36830  trer  36920  nabi1i  36998  nabi2i  36999  regsfromregtco  37142  bj-nnfbit  37476  bj-dvelimdv  37579  bj-gabima  37669  bj-elsngl  37697  bj-nuliotaALT  37787  bj-axseprep  37804  bj-rest10  37823  bj-restuni  37832  con1bii2  38071  con2bii2  38072  topdifinfeq  38089  isbasisrelowllem2  38095  wl-1xor  38221  wl-1mintru1  38227  wl-sb8eut  38326  wl-sb8eutv  38327  inixp  38463  notbinot1  38814  notbinot2  38818  truconj  38834  sbccom2lem  38857  sbccom2  38858  sbccom2f  38859  tsim1  38863  tsxo3  38872  tsxo4  38873  trcoss2  39307  dfcomember3  39492  eqvreldmqs  39493  eqvreldmqs2  39494  dfmembpart2  39606  eldisjn0el  39642  isopos  40038  islvol5  40437  elpadd0  40667  dvhopellsm  41975  diblsmopel  42029  mapdvalc  42487  3factsumint2  42873  3factsumint3  42874  3factsumint4  42875  aks4d1p1p2  42921  aks4d1p7  42934  isprimroot  42944  aks6d1c1p1  42958  aks6d1c2p2  42970  sticksstones22  43019  unitscyglem4  43049  elpwbi  43085  redvmptabs  43220  dffltz  43465  rmxypairf1o  43737  onsupmaxb  44065  ifpnotnotb  44304  ifpdfxor  44312  ifpidg  44316  ifpim123g  44325  ifpim1g  44326  ifpimimb  44329  ifpimim  44334  rp-fakeanorass  44338  elmapintrab  44401  undmrnresiss  44429  clcnvlem  44448  sqrtcvallem1  44456  cnviun  44475  dfxor4  44591  dfhe3  44600  dffrege69  44757  dffrege76  44764  or3or  44848  uneqsn  44850  mnurndlem1  45090  ismnushort  45110  pm10.252  45170  pm10.253  45171  pm10.42  45173  aaanv  45197  pm13.195  45222  pm13.196a  45223  sbc3or  45340  en3lpVD  45652  3orbi123VD  45657  sbc3orgVD  45658  sbcoreleleqVD  45666  undif3VD  45689  ax6e2ndeqVD  45716  ax6e2ndeqALT  45738  sineq0ALT  45744  n0abso  45784  permaxsep  45815  permaxinf2lem  45820  iindif2f  45977  allbutfiinf  46233  limsupequzmptlem  46541  cncfshift  46687  dvnmul  46756  dvnprodlem2  46760  rrxsnicc  47113  sge00  47189  sge0iunmpt  47231  meadjiun  47279  ovolval4lem1  47462  nsssmfmbf  47592  smfmullem4  47607  aibandbiaiffaiffb  47767  plcofph  47817  pldofph  47818  plvcofph  47819  plvcofphax  47820  plvofpos  47821  n0nsn2el  47898  fsetsniunop  47922  2reu8i  47986  aovov0bi  48069  tz6.12-afv2  48113  4an21  48143  ichbi12i  48345  ichnfimlem  48348  spr0nelg  48361  sprvalpwn0  48368  reuprpr  48408  nprmmul1  48412  requad2  48524  clnbgrel  48729  usgrexmpl2nb4  48936  pg4cyclnex  49028  copisnmnd  49069  isprmrng  49236  pgrpgt2nabl  49281  lindslinindsimp2lem5  49377  islininds2  49399  ldepslinc  49424  line2ylem  49666  alsanmo  50721  ralsanmo  50722  alsralrex  50723  2alsraln0id  50729