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  1489  nornot  1520  nororOLD  1525  truan  1544  truimfal  1557  nottru  1560  falbitru  1563  falnorfalOLD  1588  nic-dfim  1666  nic-dfneg  1667  2nalexn  1824  2nexaln  1826  equvinv  2032  cleljust  2119  sbelx  2251  sb5  2272  dfsb7OLD  2282  sb6rfv  2372  cleljustALT  2378  cleljustALT2  2379  dvelimf  2466  sb5rf  2486  sb6rf  2487  sb10f  2567  nexmo  2619  exists2  2745  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  3631  ceqsrexbv  3649  clel4  3655  rabeqc  3677  2reu5lem1  3745  2reu5lem2  3746  2reu5lem3  3747  dfsbcq2  3774  cbvreucsf  3926  nss  4028  dfdif3  4090  symdifass  4227  difab  4271  un0  4343  in0  4344  ss0b  4350  2nreu  4392  rexdifpr  4591  reuprg  4632  ssunsn2  4753  iindif2  4991  nssss  5340  snopeqop  5388  epse  5532  rnep  5791  cotrg  5965  mptpreima  6086  ralrnmpt  6856  fmptsng  6924  fmptsnd  6925  dff14a  7022  f13dfv  7025  weniso  7101  abnex  7473  uniuni  7478  suppvalbr  7828  eroveu  8386  mapsnend  8582  isfinite2  8770  marypha1lem  8891  marypha2lem4  8896  infcllem  8945  en3lplem2  9070  cantnfp1  9138  carden2  9410  fseqenlem1  9444  iscard3  9513  cardnum  9514  alephinit  9515  cardinfima  9517  alephiso  9518  dfac10b  9559  dfackm  9586  isfin5-2  9807  brdom7disj  9947  brdom6disj  9948  fsuppmapnn0fiubex  13354  hash2prb  13824  hashle2prv  13830  hashtpg  13837  swrdnnn0nd  14012  wrd2ind  14079  cshwsexa  14180  s4f1o  14274  cotr2g  14330  relexpindlem  14416  lcmfunsnlem2  15978  ncoprmlnprm  16062  vdwapun  16304  cshwsiun  16427  cshwshash  16432  grpss  18115  symgsubmefmnd  18520  pmtrfrn  18580  pmtrrn2  18582  pmtrprfvalrn  18610  issrg  19251  acsfn1p  19572  0ringnnzr  20036  unocv  20818  dsmmacl  20879  pmatcollpw2lem  21379  fvmptnn04if  21451  toptopon  21519  ordtbas2  21793  ordtrest2  21806  xmeterval  23036  isclmp  23695  ovolfcl  24061  eldv  24490  eltayl  24942  musumsum  25763  2sqreu  26026  2sqreunn  26027  2sqreult  26028  2sqreultb  26029  2sqreunnlt  26030  2sqreunnltb  26031  umgrislfupgrlem  26901  numedglnl  26923  ausgrusgrb  26944  cplgr3v  27211  vtxd0nedgb  27264  finsumvtxdg2ssteplem1  27321  isrgr  27335  rgrusgrprc  27365  rgrprcx  27368  upgr2wlk  27444  pthsfval  27496  wwlksnwwlksnon  27688  usgr2wspthon  27738  isclwwlk  27756  clwwlkvbij  27886  iseupthf1o  27975  frcond2  28040  nfrgr2v  28045  4cycl2vnunb  28063  fusgr2wsp2nb  28107  frgrregord013  28168  lejdii  29309  mdslle1i  30088  mdslle2i  30089  mdslj1i  30090  mdslj2i  30091  mo5f  30247  unipreima  30385  2ndpreima  30437  ordtrest2NEW  31161  ordtconnlem1  31162  ballotlem2  31741  plymulx0  31812  bnj115  31990  bnj156  31993  bnj206  31996  bnj110  32125  bnj121  32137  bnj124  32138  bnj130  32141  bnj153  32147  bnj207  32148  bnj581  32175  bnj611  32185  bnj864  32189  bnj865  32190  bnj893  32195  bnj1000  32208  bnj978  32216  bnj1040  32239  bnj1049  32241  bnj1133  32256  bnj1189  32276  satfv1  32605  satfvsucsuc  32607  satfdm  32611  satf0  32614  satf0op  32619  fmlafvel  32627  cnvco1  32990  cnvco2  32991  dfiota3  33379  trer  33659  nabi1i  33737  nabi2i  33738  bj-hbext  34039  bj-nnfbit  34076  bj-dvelimdv  34170  bj-denotes  34183  bj-elsngl  34275  bj-nuliotaALT  34345  bj-rest10  34373  bj-restuni  34382  con1bii2  34607  con2bii2  34608  topdifinfeq  34625  isbasisrelowllem2  34631  wl-sb8eut  34807  wl-dfralf  34833  inixp  34997  notbinot1  35351  notbinot2  35355  truconj  35373  sbccom2lem  35396  sbccom2  35397  sbccom2f  35398  tsim1  35402  tsxo3  35411  tsxo4  35412  trcoss2  35718  dfmember3  35902  eqvreldmqs  35903  isopos  36310  islvol5  36709  elpadd0  36939  dvhopellsm  38247  diblsmopel  38301  mapdvalc  38759  elpwbi  39109  dffltz  39264  rmxypairf1o  39501  ifpnotnotb  39838  ifpdfxor  39846  ifpidg  39850  ifpim123g  39859  ifpim1g  39860  ifpimimb  39863  ifpimim  39868  rp-fakeanorass  39872  elmapintrab  39929  undmrnresiss  39957  clcnvlem  39976  cnviun  39988  dfxor4  40104  dfhe3  40114  dffrege69  40271  dffrege76  40278  or3or  40364  uneqsn  40366  scottabf  40569  mnurndlem1  40610  pm10.252  40686  pm10.253  40687  pm10.42  40689  aaanv  40713  pm13.195  40738  pm13.196a  40739  sbc3or  40859  en3lpVD  41172  3orbi123VD  41177  sbc3orgVD  41178  sbcoreleleqVD  41186  undif3VD  41209  ax6e2ndeqVD  41236  ax6e2ndeqALT  41258  sineq0ALT  41264  uzwo4  41308  fompt  41446  allbutfiinf  41687  limsupequzmptlem  42002  cncfshift  42150  dvnmul  42221  dvnprodlem2  42225  rrxsnicc  42579  salexct  42611  sge00  42652  sge0iunmpt  42694  meadjiun  42742  carageneld  42778  ovncvrrp  42840  ovolval4lem1  42925  vonioo  42958  vonicc  42961  nsssmfmbf  43049  smfmullem4  43063  aibandbiaiffaiffb  43124  plcofph  43174  pldofph  43175  plvcofph  43176  plvcofphax  43177  plvofpos  43178  2reu8i  43306  aovov0bi  43389  tz6.12-afv2  43433  4an21  43463  dfich2ai  43608  ichbi12i  43612  spr0nelg  43632  sprvalpwn0  43639  reuprpr  43679  requad2  43782  copisnmnd  44070  pgrpgt2nabl  44408  lindslinindsimp2lem5  44511  islininds2  44533  ldepslinc  44558  line2ylem  44732