Theorem bicomi 223

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

Syntax hints:   ↔ wb 205

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 206

This theorem is referenced by:  biimpri  227  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  357  nbn  373  xor3  384  pm5.41  392  pm4.63  399  pm4.61  406  pm4.76  520  anidm  566  an21  643  an43  657  anabs1  661  anabs7  663  pm4.87  842  pm4.64  848  pm4.25  905  pm4.77  962  pm4.53  985  pm4.55  987  pm4.56  988  pm4.57  990  pm5.63  1019  3anor  1109  3oran  1110  syl3anbr  1163  3an6  1447  nanbi  1499  nornot  1533  truan  1553  truimfal  1566  nottru  1569  falbitru  1572  nic-dfim  1672  nic-dfneg  1673  2nalexn  1831  2nexaln  1833  equvinv  2033  cleljust  2116  sbelx  2246  sb5OLD  2269  sb6rfv  2354  cleljustALT  2362  cleljustALT2  2363  dvelimf  2448  sb5rf  2467  sb6rf  2468  sb10f  2527  nexmo  2536  exists2  2658  cleljustab  2713  eqabdv  2868  eqabcri  2879  nfabdwOLD  2928  nne  2945  necon3bbii  2989  necon2abii  2992  necon2bbii  2993  nnel  3057  nelbOLD  3233  ralcom4OLD  3285  rspc2gv  3622  ceqsrexbv  3645  clel4OLD  3655  rabeqcOLD  3682  2reu5lem1  3752  2reu5lem2  3753  2reu5lem3  3754  dfsbcq2  3781  cbvreucsf  3941  nss  4047  ss2abdv  4061  dfdif3  4115  symdifass  4252  indifdi  4284  difab  4301  neq0  4346  ab0OLD  4376  un0  4391  in0  4392  ss0b  4398  eq0rdv  4405  2nreu  4442  ralidm  4512  ralf0  4514  rexdifpr  4662  reuprg  4708  snssb  4787  snssg  4788  ssunsn2  4831  iindif2  5081  eqsnuniex  5360  nssss  5456  snopeqop  5507  dffr6  5635  epse  5660  rnep  5927  cotrgOLDOLD  6111  mptpreima  6238  ralrnmpt  7098  fmptsng  7166  fmptsnd  7167  dff14a  7269  f13dfv  7272  weniso  7351  abnex  7744  uniuni  7749  frpoins3xp3g  8127  xpord3inddlem  8140  eroveu  8806  fsetexb  8858  mapsnend  9036  isfinite2  9301  marypha1lem  9428  marypha2lem4  9433  infcllem  9482  en3lplem2  9608  cantnfp1  9676  carden2  9982  fseqenlem1  10019  iscard3  10088  cardnum  10089  alephinit  10090  cardinfima  10092  alephiso  10093  dfac10b  10134  dfackm  10161  isfin5-2  10386  brdom7disj  10526  brdom6disj  10527  fsuppmapnn0fiubex  13957  hash2prb  14433  hashle2prv  14439  hashtpg  14446  swrdnnn0nd  14606  wrd2ind  14673  cshwsexaOLD  14775  s4f1o  14869  cotr2g  14923  relexpindlem  15010  lcmfunsnlem2  16577  ncoprmlnprm  16664  vdwapun  16907  cshwsiun  17033  cshwshash  17038  grpss  18840  symgsubmefmnd  19266  pmtrfrn  19326  pmtrrn2  19328  pmtrprfvalrn  19356  issrg  20011  0ringnnzr  20302  acsfn1p  20415  df2idl2  20860  unocv  21233  dsmmacl  21296  pmatcollpw2lem  22279  fvmptnn04if  22351  toptopon  22419  ordtbas2  22695  ordtrest2  22708  xmeterval  23938  isclmp  24613  ovolfcl  24983  eldv  25415  eltayl  25872  musumsum  26696  2sqreu  26959  2sqreunn  26960  2sqreult  26961  2sqreultb  26962  2sqreunnlt  26963  2sqreunnltb  26964  nosupinfsep  27235  umgrislfupgrlem  28413  numedglnl  28435  ausgrusgrb  28456  cplgr3v  28723  vtxd0nedgb  28776  finsumvtxdg2ssteplem1  28833  isrgr  28847  rgrusgrprc  28877  rgrprcx  28880  upgr2wlk  28956  wwlksnwwlksnon  29200  usgr2wspthon  29250  isclwwlk  29268  clwwlkvbij  29397  iseupthf1o  29486  frcond2  29551  nfrgr2v  29556  4cycl2vnunb  29574  fusgr2wsp2nb  29618  frgrregord013  29679  lejdii  30822  mdslle1i  31601  mdslle2i  31602  mdslj1i  31603  mdslj2i  31604  mo5f  31760  unipreima  31900  2ndpreima  31960  mgccnv  32200  quslsm  32547  ordtrest2NEW  32934  ordtconnlem1  32935  ballotlem2  33518  plymulx0  33589  bnj115  33767  bnj156  33770  bnj206  33773  bnj110  33900  bnj121  33912  bnj124  33913  bnj130  33916  bnj153  33922  bnj207  33923  bnj581  33950  bnj611  33960  bnj864  33964  bnj865  33965  bnj893  33970  bnj1000  33983  bnj978  33991  bnj1040  34014  bnj1049  34016  bnj1133  34031  bnj1189  34051  satfv1  34385  satfvsucsuc  34387  satfdm  34391  satf0  34394  satf0op  34399  fmlafvel  34407  cnvco1  34760  cnvco2  34761  dfiota3  34926  trer  35249  nabi1i  35327  nabi2i  35328  bj-hbext  35636  bj-nnfbit  35678  bj-dvelimdv  35778  bj-gabima  35868  bj-elsngl  35897  bj-nuliotaALT  35987  bj-rest10  36017  bj-restuni  36026  con1bii2  36261  con2bii2  36262  topdifinfeq  36279  isbasisrelowllem2  36285  wl-1xor  36411  wl-1mintru1  36417  wl-sb8eut  36490  inixp  36644  notbinot1  36995  notbinot2  36999  truconj  37017  sbccom2lem  37040  sbccom2  37041  sbccom2f  37042  tsim1  37046  tsxo3  37055  tsxo4  37056  trcoss2  37402  dfcomember3  37592  eqvreldmqs  37593  eqvreldmqs2  37594  dfmembpart2  37688  eldisjn0el  37724  isopos  38098  islvol5  38498  elpadd0  38728  dvhopellsm  40036  diblsmopel  40090  mapdvalc  40548  3factsumint2  40935  3factsumint3  40936  3factsumint4  40937  aks4d1p1p2  40983  aks4d1p7  40996  aks6d1c2p2  41005  sticksstones22  41032  elpwbi  41097  dffltz  41424  rmxypairf1o  41698  onsupmaxb  42036  ifpnotnotb  42278  ifpdfxor  42286  ifpidg  42290  ifpim123g  42299  ifpim1g  42300  ifpimimb  42303  ifpimim  42308  rp-fakeanorass  42312  elmapintrab  42375  undmrnresiss  42403  clcnvlem  42422  sqrtcvallem1  42430  cnviun  42449  dfxor4  42565  dfhe3  42574  dffrege69  42731  dffrege76  42738  or3or  42822  uneqsn  42824  scottabf  43047  mnurndlem1  43088  ismnushort  43108  pm10.252  43168  pm10.253  43169  pm10.42  43171  aaanv  43195  pm13.195  43220  pm13.196a  43221  sbc3or  43341  en3lpVD  43654  3orbi123VD  43659  sbc3orgVD  43660  sbcoreleleqVD  43668  undif3VD  43691  ax6e2ndeqVD  43718  ax6e2ndeqALT  43740  sineq0ALT  43746  uzwo4  43788  iindif2f  43902  fompt  43938  allbutfiinf  44178  limsupequzmptlem  44492  cncfshift  44638  dvnmul  44707  dvnprodlem2  44711  rrxsnicc  45064  salexct  45098  sge00  45140  sge0iunmpt  45182  meadjiun  45230  carageneld  45266  ovncvrrp  45328  ovolval4lem1  45413  vonioo  45446  vonicc  45449  nsssmfmbf  45543  smfmullem4  45558  aibandbiaiffaiffb  45652  plcofph  45702  pldofph  45703  plvcofph  45704  plvcofphax  45705  plvofpos  45706  n0nsn2el  45783  fsetsniunop  45807  2reu8i  45869  aovov0bi  45952  tz6.12-afv2  45996  4an21  46026  ichbi12i  46176  ichnfimlem  46179  spr0nelg  46192  sprvalpwn0  46199  reuprpr  46239  requad2  46339  copisnmnd  46627  pgrpgt2nabl  47090  lindslinindsimp2lem5  47191  islininds2  47213  ldepslinc  47238  line2ylem  47485