Theorem bicomi 224

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

Syntax hints:   ↔ wb 206

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 207

This theorem is referenced by:  biimpri  228  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  356  nbn  372  xor3  382  pm5.41  390  pm4.63  397  pm4.61  404  pm4.76  518  anidm  564  an21  645  an43  659  anabs1  663  anabs7  665  pm4.87  844  pm4.64  850  pm4.25  906  pm4.77  965  pm4.53  988  pm4.55  990  pm4.56  991  pm4.57  993  pm5.63  1022  3anor  1108  3oran  1109  syl3anbr  1163  3an6  1449  nanbi  1502  nornot  1533  truan  1553  truimfal  1566  nottru  1569  falbitru  1572  nic-dfim  1671  nic-dfneg  1672  2nalexn  1830  2nexaln  1832  equvinv  2031  cleljust  2123  sbelx  2261  sb6rfv  2362  cleljustALT  2369  cleljustALT2  2370  dvelimf  2453  sb5rf  2472  sb6rf  2473  sb10f  2532  nexmo  2542  exists2  2663  cleljustab  2718  eqabdv  2870  eqabcri  2880  nne  2937  necon3bbii  2980  necon2abii  2983  necon2bbii  2984  nnel  3047  r19.41v  3167  r3ex  3176  r19.41  3241  rspc2gv  3587  ceqsrexbv  3611  2reu5lem1  3714  2reu5lem2  3715  2reu5lem3  3716  dfsbcq2  3744  cbvreucsf  3894  nss  3999  dfdif3OLD  4071  symdifass  4215  indifdi  4247  difab  4263  neq0  4305  un0  4347  in0  4348  ss0b  4354  2nreu  4397  ralidm  4471  reuprg  4661  snssb  4740  snssg  4741  ssunsn2  4784  iindif2  5033  eqsnuniex  5307  nssss  5404  snopeqop  5455  dffr6  5581  epse  5607  rnep  5877  mptpreima  6197  ralrnmpt  7043  fmptsng  7117  fmptsnd  7118  dff14a  7219  f13dfv  7223  weniso  7303  abnex  7705  uniuni  7710  frpoins3xp3g  8086  xpord3inddlem  8099  eroveu  8754  fsetexb  8806  mapsnend  8978  isfinite2  9203  marypha1lem  9341  marypha2lem4  9346  infcllem  9396  en3lplem2  9527  cantnfp1  9595  carden2  9904  fseqenlem1  9939  iscard3  10008  cardnum  10009  alephinit  10010  cardinfima  10012  alephiso  10013  dfac10b  10055  dfackm  10082  isfin5-2  10306  brdom7disj  10446  brdom6disj  10447  fsuppmapnn0fiubex  13920  hash2prb  14400  hashle2prv  14406  hashtpg  14413  hash3tpb  14423  swrdnnn0nd  14585  wrd2ind  14651  s4f1o  14846  cotr2g  14904  relexpindlem  14991  lcmfunsnlem2  16572  ncoprmlnprm  16660  vdwapun  16907  cshwsiun  17032  cshwshash  17037  grpss  18889  symgsubmefmnd  19332  pmtrfrn  19392  pmtrrn2  19394  pmtrprfvalrn  19422  issrg  20128  0ringnnzr  20463  acsfn1p  20737  unocv  21640  dsmmacl  21701  pmatcollpw2lem  22726  fvmptnn04if  22798  toptopon  22866  ordtbas2  23140  ordtrest2  23153  xmeterval  24381  isclmp  25058  ovolfcl  25428  eldv  25860  eltayl  26328  musumsum  27163  2sqreu  27428  2sqreunn  27429  2sqreult  27430  2sqreultb  27431  2sqreunnlt  27432  2sqreunnltb  27433  nosupinfsep  27705  umgrislfupgrlem  29200  numedglnl  29222  ausgrusgrb  29243  cplgr3v  29513  vtxd0nedgb  29567  finsumvtxdg2ssteplem1  29624  isrgr  29638  rgrusgrprc  29668  rgrprcx  29671  upgr2wlk  29745  dfpth2  29807  wwlksnwwlksnon  29993  usgr2wspthon  30046  isclwwlk  30064  clwwlkvbij  30193  iseupthf1o  30282  frcond2  30347  nfrgr2v  30352  4cycl2vnunb  30370  fusgr2wsp2nb  30414  frgrregord013  30475  lejdii  31618  mdslle1i  32397  mdslle2i  32398  mdslj1i  32399  mdslj2i  32400  mo5f  32567  n0nsnel  32594  unipreima  32725  2ndpreima  32790  mgccnv  33084  domnprodeq0  33362  quslsm  33490  mplmonprod  33723  ordtrest2NEW  34093  ordtconnlem1  34094  ballotlem2  34659  plymulx0  34717  bnj115  34894  bnj156  34897  bnj206  34900  bnj110  35027  bnj121  35039  bnj124  35040  bnj130  35043  bnj153  35049  bnj207  35050  bnj581  35077  bnj611  35087  bnj864  35091  bnj865  35092  bnj893  35097  bnj1000  35110  bnj978  35118  bnj1040  35141  bnj1049  35143  bnj1133  35158  bnj1189  35178  satfv1  35570  satfvsucsuc  35572  satfdm  35576  satf0  35579  satf0op  35584  fmlafvel  35592  cnvco1  35966  cnvco2  35967  dfiota3  36128  ss-ax8  36432  trer  36523  nabi1i  36601  nabi2i  36602  regsfromregtr  36681  bj-hbext  36924  bj-nnfbit  36966  bj-dvelimdv  37065  bj-gabima  37154  bj-elsngl  37182  bj-nuliotaALT  37272  bj-rest10  37306  bj-restuni  37315  con1bii2  37550  con2bii2  37551  topdifinfeq  37568  isbasisrelowllem2  37574  wl-1xor  37700  wl-1mintru1  37706  wl-sb8eut  37796  wl-sb8eutv  37797  inixp  37942  notbinot1  38293  notbinot2  38297  truconj  38315  sbccom2lem  38338  sbccom2  38339  sbccom2f  38340  tsim1  38344  tsxo3  38353  tsxo4  38354  trcoss2  38788  dfcomember3  38973  eqvreldmqs  38974  eqvreldmqs2  38975  dfmembpart2  39087  eldisjn0el  39123  isopos  39519  islvol5  39918  elpadd0  40148  dvhopellsm  41456  diblsmopel  41510  mapdvalc  41968  3factsumint2  42355  3factsumint3  42356  3factsumint4  42357  aks4d1p1p2  42403  aks4d1p7  42416  isprimroot  42426  aks6d1c1p1  42440  aks6d1c2p2  42452  sticksstones22  42501  unitscyglem4  42531  elpwbi  42565  redvmptabs  42693  dffltz  42955  rmxypairf1o  43231  onsupmaxb  43559  ifpnotnotb  43798  ifpdfxor  43806  ifpidg  43810  ifpim123g  43819  ifpim1g  43820  ifpimimb  43823  ifpimim  43828  rp-fakeanorass  43832  elmapintrab  43895  undmrnresiss  43923  clcnvlem  43942  sqrtcvallem1  43950  cnviun  43969  dfxor4  44085  dfhe3  44094  dffrege69  44251  dffrege76  44258  or3or  44342  uneqsn  44344  scottabf  44559  mnurndlem1  44600  ismnushort  44620  pm10.252  44680  pm10.253  44681  pm10.42  44683  aaanv  44707  pm13.195  44732  pm13.196a  44733  sbc3or  44851  en3lpVD  45163  3orbi123VD  45168  sbc3orgVD  45169  sbcoreleleqVD  45177  undif3VD  45200  ax6e2ndeqVD  45227  ax6e2ndeqALT  45249  sineq0ALT  45255  n0abso  45295  permaxsep  45326  permaxinf2lem  45331  uzwo4  45376  iindif2f  45482  allbutfiinf  45741  limsupequzmptlem  46049  cncfshift  46195  dvnmul  46264  dvnprodlem2  46268  rrxsnicc  46621  salexct  46655  sge00  46697  sge0iunmpt  46739  meadjiun  46787  carageneld  46823  ovncvrrp  46885  ovolval4lem1  46970  vonioo  47003  vonicc  47006  nsssmfmbf  47100  smfmullem4  47115  aibandbiaiffaiffb  47217  plcofph  47267  pldofph  47268  plvcofph  47269  plvcofphax  47270  plvofpos  47271  n0nsn2el  47348  fsetsniunop  47372  2reu8i  47436  aovov0bi  47519  tz6.12-afv2  47563  4an21  47593  ichbi12i  47783  ichnfimlem  47786  spr0nelg  47799  sprvalpwn0  47806  reuprpr  47846  requad2  47946  clnbgrel  48151  usgrexmpl2nb4  48358  pg4cyclnex  48450  copisnmnd  48492  pgrpgt2nabl  48689  lindslinindsimp2lem5  48785  islininds2  48807  ldepslinc  48832  line2ylem  49074