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  394  pm4.63  402  pm4.61  409  pm4.76  527  anidm  574  an21  656  an43  670  anabs1  674  anabs7  676  pm4.87  856  pm4.64  862  pm4.25  918  pm4.77  976  pm4.53  1000  pm4.55  1002  pm4.56  1003  pm4.57  1005  pm5.63  1036  3anor  1124  3oran  1125  syl3anbr  1179  3an6  1474  nanbi  1529  nornot  1560  truan  1580  truimfal  1593  nottru  1596  falbitru  1599  nic-dfim  1698  nic-dfneg  1699  2nalexn  1857  2nexaln  1859  equvinv  2058  cleljust  2151  sbelx  2288  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  3590  ceqsrexbv  3614  2reu5lem1  3717  2reu5lem2  3718  2reu5lem3  3719  dfsbcq2  3746  cbvreucsf  3896  nss  4000  dfdif3OLD  4072  symdifass  4214  indifdi  4246  difab  4262  neq0  4305  un0  4350  in0  4351  ss0b  4357  2nreu  4408  ralidm  4477  reuprg  4668  snssb  4747  snssg  4748  ssunsn2  4792  iindif2  5042  eqsnuniex  5331  nssss  5435  snopeqop  5488  dffr6  5616  epse  5642  rnep  5916  mptpreima  6238  ralrnmpt  7091  fmptsng  7166  fmptsnd  7167  dff14a  7268  f13dfv  7272  weniso  7354  abnex  7754  uniuni  7759  frpoins3xp3g  8135  xpord3inddlem  8148  eroveu  8808  fsetexb  8859  mapsnend  9031  isfinite2  9256  marypha1lem  9391  marypha2lem4  9396  infcllem  9446  en3lplem2  9580  cantnfp1  9648  scottabf  9866  carden2  9980  fseqenlem1  10015  iscard3  10084  cardnum  10085  alephinit  10086  cardinfima  10088  alephiso  10089  dfac10b  10130  dfackm  10157  isfin5-2  10381  brdom7disj  10521  brdom6disj  10522  fsuppmapnn0fiubex  14035  hash2prb  14516  hashle2prv  14522  hashtpg  14529  hash3tpb  14539  swrdnnn0nd  14701  wrd2ind  14767  s4f1o  14962  cotr2g  15020  relexpindlem  15107  lcmfunsnlem2  16704  ncoprmlnprm  16793  vdwapun  17040  cshwsiun  17165  cshwshash  17170  grpss  19027  symgsubmefmnd  19474  pmtrfrn  19534  pmtrrn2  19536  pmtrprfvalrn  19564  issrg  20276  0ringnnzr  20634  acsfn1p  20913  unocv  21841  dsmmacl  21902  pmatcollpw2lem  22945  fvmptnn04if  23017  toptopon  23085  ordtbas2  23359  ordtrest2  23372  xmeterval  24600  isclmp  25267  ovolfcl  25636  eldv  26068  plyn0mulidp  26453  eltayl  26534  musumsum  27367  2sqreu  27631  2sqreunn  27632  2sqreult  27633  2sqreultb  27634  2sqreunnlt  27635  2sqreunnltb  27636  nosupinfsep  27907  umgrislfupgrlem  29483  numedglnl  29505  ausgrusgrb  29526  cplgr3v  29796  vtxd0nedgb  29849  finsumvtxdg2ssteplem1  29906  isrgr  29920  rgrusgrprc  29950  rgrprcx  29953  upgr2wlk  30027  dfpth2  30089  wwlksnwwlksnon  30275  usgr2wspthon  30328  isclwwlk  30346  clwwlkvbij  30475  iseupthf1o  30564  frcond2  30629  nfrgr2v  30634  4cycl2vnunb  30652  fusgr2wsp2nb  30696  frgrregord013  30757  lejdii  31901  mdslle1i  32680  mdslle2i  32681  mdslj1i  32682  mdslj2i  32683  mo5f  32846  n0nsnel  32872  unipreima  32999  2ndpreima  33064  mgccnv  33328  domnprodeq0  33608  quslsm  33723  mplmonprod  33953  ordtrest2NEW  34322  ordtconnlem1  34323  ballotlem2  34888  bnj115  35123  bnj156  35126  bnj206  35129  bnj110  35255  bnj121  35267  bnj124  35268  bnj130  35271  bnj153  35277  bnj207  35278  bnj581  35305  bnj611  35315  bnj864  35319  bnj865  35320  bnj893  35325  bnj1000  35338  bnj978  35346  bnj1040  35369  bnj1049  35371  bnj1133  35386  bnj1189  35406  satfv1  35863  satfvsucsuc  35865  satfdm  35869  satf0  35872  satf0op  35877  fmlafvel  35885  cnvco1  36259  cnvco2  36260  dfiota3  36421  ss-ax8  36765  trer  36855  nabi1i  36933  nabi2i  36934  regsfromregtco  37077  bj-nnfbit  37411  bj-dvelimdv  37514  bj-gabima  37604  bj-elsngl  37632  bj-nuliotaALT  37722  bj-axseprep  37739  bj-rest10  37758  bj-restuni  37767  con1bii2  38006  con2bii2  38007  topdifinfeq  38024  isbasisrelowllem2  38030  wl-1xor  38156  wl-1mintru1  38162  wl-sb8eut  38261  wl-sb8eutv  38262  inixp  38407  notbinot1  38758  notbinot2  38762  truconj  38778  sbccom2lem  38801  sbccom2  38802  sbccom2f  38803  tsim1  38807  tsxo3  38816  tsxo4  38817  trcoss2  39251  dfcomember3  39436  eqvreldmqs  39437  eqvreldmqs2  39438  dfmembpart2  39550  eldisjn0el  39586  isopos  39982  islvol5  40381  elpadd0  40611  dvhopellsm  41919  diblsmopel  41973  mapdvalc  42431  3factsumint2  42817  3factsumint3  42818  3factsumint4  42819  aks4d1p1p2  42865  aks4d1p7  42878  isprimroot  42888  aks6d1c1p1  42902  aks6d1c2p2  42914  sticksstones22  42963  unitscyglem4  42993  elpwbi  43029  redvmptabs  43149  dffltz  43394  rmxypairf1o  43666  onsupmaxb  43994  ifpnotnotb  44233  ifpdfxor  44241  ifpidg  44245  ifpim123g  44254  ifpim1g  44255  ifpimimb  44258  ifpimim  44263  rp-fakeanorass  44267  elmapintrab  44330  undmrnresiss  44358  clcnvlem  44377  sqrtcvallem1  44385  cnviun  44404  dfxor4  44520  dfhe3  44529  dffrege69  44686  dffrege76  44693  or3or  44777  uneqsn  44779  mnurndlem1  45019  ismnushort  45039  pm10.252  45099  pm10.253  45100  pm10.42  45102  aaanv  45126  pm13.195  45151  pm13.196a  45152  sbc3or  45269  en3lpVD  45581  3orbi123VD  45586  sbc3orgVD  45587  sbcoreleleqVD  45595  undif3VD  45618  ax6e2ndeqVD  45645  ax6e2ndeqALT  45667  sineq0ALT  45673  n0abso  45713  permaxsep  45744  permaxinf2lem  45749  iindif2f  45906  allbutfiinf  46162  limsupequzmptlem  46470  cncfshift  46616  dvnmul  46685  dvnprodlem2  46689  rrxsnicc  47042  sge00  47118  sge0iunmpt  47160  meadjiun  47208  ovolval4lem1  47391  nsssmfmbf  47521  smfmullem4  47536  aibandbiaiffaiffb  47659  plcofph  47709  pldofph  47710  plvcofph  47711  plvcofphax  47712  plvofpos  47713  n0nsn2el  47790  fsetsniunop  47814  2reu8i  47878  aovov0bi  47961  tz6.12-afv2  48005  4an21  48035  ichbi12i  48237  ichnfimlem  48240  spr0nelg  48253  sprvalpwn0  48260  reuprpr  48300  nprmmul1  48304  requad2  48416  clnbgrel  48621  usgrexmpl2nb4  48828  pg4cyclnex  48920  copisnmnd  48962  isprmrng  49129  pgrpgt2nabl  49174  lindslinindsimp2lem5  49270  islininds2  49292  ldepslinc  49317  line2ylem  49559  alsanmo  50616  ralsanmo  50617  alsralrex  50618  2alsraln0id  50624