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  syl5bbr  287  syl5rbbr  288  syl6bbr  291  syl6rbbr  292  mtbir  325  sylnibr  331  sylnbir  333  xchnxbir  335  xchbinxr  337  con1bii  359  nbn  375  xor3  386  pm5.41  394  pm4.63  400  pm4.61  407  pm4.76  521  anidm  567  an21  642  an43  656  anabs1  660  anabs7  662  pm4.87  839  pm4.64  845  pm4.25  902  pm4.77  959  pm4.53  982  pm4.55  984  pm4.56  985  pm4.57  987  pm5.63  1016  3anor  1104  3oran  1105  syl3anbr  1158  3an6  1442  nanbi  1490  nornot  1524  nororOLD  1529  truan  1548  truimfal  1561  nottru  1564  falbitru  1567  falnorfalOLD  1592  nic-dfim  1670  nic-dfneg  1671  2nalexn  1828  2nexaln  1830  equvinv  2036  cleljust  2123  sbelx  2255  sb5  2276  dfsb7OLD  2286  sb6rfv  2376  cleljustALT  2382  cleljustALT2  2383  dvelimf  2470  sb5rf  2490  sb6rf  2491  sb10f  2571  nexmo  2623  exists2  2747  cleljustab  2802  abeq1i  2949  abbi2dv  2950  nfabdw  3000  nne  3020  necon3bbii  3063  necon2abii  3066  necon2bbii  3067  nnel  3132  ralcom4  3235  rexcom4  3249  nelb  3268  rspc2gv  3632  ceqsrexbv  3650  clel4  3656  rabeqc  3678  2reu5lem1  3746  2reu5lem2  3747  2reu5lem3  3748  dfsbcq2  3775  cbvreucsf  3927  nss  4029  dfdif3  4091  symdifass  4228  difab  4272  un0  4344  in0  4345  ss0b  4351  2nreu  4393  rexdifpr  4598  reuprg  4639  ssunsn2  4760  iindif2  4999  nssss  5348  snopeqop  5396  epse  5538  rnep  5797  cotrg  5971  mptpreima  6092  ralrnmpt  6862  fmptsng  6930  fmptsnd  6931  dff14a  7028  f13dfv  7031  weniso  7107  abnex  7479  uniuni  7484  suppvalbr  7834  eroveu  8392  mapsnend  8588  isfinite2  8776  marypha1lem  8897  marypha2lem4  8902  infcllem  8951  en3lplem2  9076  cantnfp1  9144  carden2  9416  fseqenlem1  9450  iscard3  9519  cardnum  9520  alephinit  9521  cardinfima  9523  alephiso  9524  dfac10b  9565  dfackm  9592  isfin5-2  9813  brdom7disj  9953  brdom6disj  9954  fsuppmapnn0fiubex  13361  hash2prb  13831  hashle2prv  13837  hashtpg  13844  swrdnnn0nd  14018  wrd2ind  14085  cshwsexa  14186  s4f1o  14280  cotr2g  14336  relexpindlem  14422  lcmfunsnlem2  15984  ncoprmlnprm  16068  vdwapun  16310  cshwsiun  16433  cshwshash  16438  grpss  18121  symgsubmefmnd  18526  pmtrfrn  18586  pmtrrn2  18588  pmtrprfvalrn  18616  issrg  19257  acsfn1p  19578  0ringnnzr  20042  unocv  20824  dsmmacl  20885  pmatcollpw2lem  21385  fvmptnn04if  21457  toptopon  21525  ordtbas2  21799  ordtrest2  21812  xmeterval  23042  isclmp  23701  ovolfcl  24067  eldv  24496  eltayl  24948  musumsum  25769  2sqreu  26032  2sqreunn  26033  2sqreult  26034  2sqreultb  26035  2sqreunnlt  26036  2sqreunnltb  26037  umgrislfupgrlem  26907  numedglnl  26929  ausgrusgrb  26950  cplgr3v  27217  vtxd0nedgb  27270  finsumvtxdg2ssteplem1  27327  isrgr  27341  rgrusgrprc  27371  rgrprcx  27374  upgr2wlk  27450  pthsfval  27502  wwlksnwwlksnon  27694  usgr2wspthon  27744  isclwwlk  27762  clwwlkvbij  27892  iseupthf1o  27981  frcond2  28046  nfrgr2v  28051  4cycl2vnunb  28069  fusgr2wsp2nb  28113  frgrregord013  28174  lejdii  29315  mdslle1i  30094  mdslle2i  30095  mdslj1i  30096  mdslj2i  30097  mo5f  30253  unipreima  30391  2ndpreima  30443  ordtrest2NEW  31166  ordtconnlem1  31167  ballotlem2  31746  plymulx0  31817  bnj115  31995  bnj156  31998  bnj206  32001  bnj110  32130  bnj121  32142  bnj124  32143  bnj130  32146  bnj153  32152  bnj207  32153  bnj581  32180  bnj611  32190  bnj864  32194  bnj865  32195  bnj893  32200  bnj1000  32213  bnj978  32221  bnj1040  32244  bnj1049  32246  bnj1133  32261  bnj1189  32281  satfv1  32610  satfvsucsuc  32612  satfdm  32616  satf0  32619  satf0op  32624  fmlafvel  32632  cnvco1  32995  cnvco2  32996  dfiota3  33384  trer  33664  nabi1i  33742  nabi2i  33743  bj-hbext  34044  bj-nnfbit  34081  bj-dvelimdv  34175  bj-elsngl  34283  bj-nuliotaALT  34354  bj-rest10  34382  bj-restuni  34391  con1bii2  34616  con2bii2  34617  topdifinfeq  34634  isbasisrelowllem2  34640  wl-sb8eut  34828  wl-dfralf  34854  inixp  35018  notbinot1  35372  notbinot2  35376  truconj  35394  sbccom2lem  35417  sbccom2  35418  sbccom2f  35419  tsim1  35423  tsxo3  35432  tsxo4  35433  trcoss2  35739  dfmember3  35923  eqvreldmqs  35924  isopos  36331  islvol5  36730  elpadd0  36960  dvhopellsm  38268  diblsmopel  38322  mapdvalc  38780  elpwbi  39165  dffltz  39320  rmxypairf1o  39557  ifpnotnotb  39894  ifpdfxor  39902  ifpidg  39906  ifpim123g  39915  ifpim1g  39916  ifpimimb  39919  ifpimim  39924  rp-fakeanorass  39928  elmapintrab  39985  undmrnresiss  40013  clcnvlem  40032  cnviun  40044  dfxor4  40160  dfhe3  40170  dffrege69  40327  dffrege76  40334  or3or  40420  uneqsn  40422  scottabf  40625  mnurndlem1  40666  pm10.252  40742  pm10.253  40743  pm10.42  40745  aaanv  40769  pm13.195  40794  pm13.196a  40795  sbc3or  40915  en3lpVD  41228  3orbi123VD  41233  sbc3orgVD  41234  sbcoreleleqVD  41242  undif3VD  41265  ax6e2ndeqVD  41292  ax6e2ndeqALT  41314  sineq0ALT  41320  uzwo4  41364  fompt  41502  allbutfiinf  41743  limsupequzmptlem  42058  cncfshift  42206  dvnmul  42277  dvnprodlem2  42281  rrxsnicc  42634  salexct  42666  sge00  42707  sge0iunmpt  42749  meadjiun  42797  carageneld  42833  ovncvrrp  42895  ovolval4lem1  42980  vonioo  43013  vonicc  43016  nsssmfmbf  43104  smfmullem4  43118  aibandbiaiffaiffb  43179  plcofph  43229  pldofph  43230  plvcofph  43231  plvcofphax  43232  plvofpos  43233  2reu8i  43361  aovov0bi  43444  tz6.12-afv2  43488  4an21  43518  dfich2ai  43663  ichbi12i  43667  spr0nelg  43687  sprvalpwn0  43694  reuprpr  43734  requad2  43837  copisnmnd  44125  pgrpgt2nabl  44463  lindslinindsimp2lem5  44566  islininds2  44588  ldepslinc  44613  line2ylem  44787