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  3168  r3ex  3177  r19.41  3242  rspc2gv  3575  ceqsrexbv  3599  2reu5lem1  3702  2reu5lem2  3703  2reu5lem3  3704  dfsbcq2  3732  cbvreucsf  3882  nss  3987  dfdif3OLD  4059  symdifass  4203  indifdi  4235  difab  4251  neq0  4293  un0  4335  in0  4336  ss0b  4342  2nreu  4385  ralidm  4458  reuprg  4648  snssb  4727  snssg  4728  ssunsn2  4771  iindif2  5020  eqsnuniex  5296  nssss  5400  snopeqop  5452  dffr6  5578  epse  5604  rnep  5874  mptpreima  6194  ralrnmpt  7040  fmptsng  7114  fmptsnd  7115  dff14a  7216  f13dfv  7220  weniso  7300  abnex  7702  uniuni  7707  frpoins3xp3g  8082  xpord3inddlem  8095  eroveu  8750  fsetexb  8802  mapsnend  8974  isfinite2  9199  marypha1lem  9337  marypha2lem4  9342  infcllem  9392  en3lplem2  9523  cantnfp1  9591  carden2  9900  fseqenlem1  9935  iscard3  10004  cardnum  10005  alephinit  10006  cardinfima  10008  alephiso  10009  dfac10b  10051  dfackm  10078  isfin5-2  10302  brdom7disj  10442  brdom6disj  10443  fsuppmapnn0fiubex  13916  hash2prb  14396  hashle2prv  14402  hashtpg  14409  hash3tpb  14419  swrdnnn0nd  14581  wrd2ind  14647  s4f1o  14842  cotr2g  14900  relexpindlem  14987  lcmfunsnlem2  16568  ncoprmlnprm  16656  vdwapun  16903  cshwsiun  17028  cshwshash  17033  grpss  18888  symgsubmefmnd  19331  pmtrfrn  19391  pmtrrn2  19393  pmtrprfvalrn  19421  issrg  20127  0ringnnzr  20460  acsfn1p  20734  unocv  21637  dsmmacl  21698  pmatcollpw2lem  22720  fvmptnn04if  22792  toptopon  22860  ordtbas2  23134  ordtrest2  23147  xmeterval  24375  isclmp  25042  ovolfcl  25411  eldv  25843  eltayl  26307  musumsum  27142  2sqreu  27407  2sqreunn  27408  2sqreult  27409  2sqreultb  27410  2sqreunnlt  27411  2sqreunnltb  27412  nosupinfsep  27684  umgrislfupgrlem  29179  numedglnl  29201  ausgrusgrb  29222  cplgr3v  29492  vtxd0nedgb  29546  finsumvtxdg2ssteplem1  29603  isrgr  29617  rgrusgrprc  29647  rgrprcx  29650  upgr2wlk  29724  dfpth2  29786  wwlksnwwlksnon  29972  usgr2wspthon  30025  isclwwlk  30043  clwwlkvbij  30172  iseupthf1o  30261  frcond2  30326  nfrgr2v  30331  4cycl2vnunb  30349  fusgr2wsp2nb  30393  frgrregord013  30454  lejdii  31598  mdslle1i  32377  mdslle2i  32378  mdslj1i  32379  mdslj2i  32380  mo5f  32547  n0nsnel  32574  unipreima  32705  2ndpreima  32770  mgccnv  33064  domnprodeq0  33342  quslsm  33470  mplmonprod  33703  ordtrest2NEW  34073  ordtconnlem1  34074  ballotlem2  34639  plymulx0  34697  bnj115  34874  bnj156  34877  bnj206  34880  bnj110  35006  bnj121  35018  bnj124  35019  bnj130  35022  bnj153  35028  bnj207  35029  bnj581  35056  bnj611  35066  bnj864  35070  bnj865  35071  bnj893  35076  bnj1000  35089  bnj978  35097  bnj1040  35120  bnj1049  35122  bnj1133  35137  bnj1189  35157  satfv1  35551  satfvsucsuc  35553  satfdm  35557  satf0  35560  satf0op  35565  fmlafvel  35573  cnvco1  35947  cnvco2  35948  dfiota3  36109  ss-ax8  36413  trer  36504  nabi1i  36582  nabi2i  36583  regsfromregtco  36726  bj-nnfbit  37053  bj-dvelimdv  37156  bj-gabima  37245  bj-elsngl  37273  bj-nuliotaALT  37363  bj-axseprep  37379  bj-rest10  37398  bj-restuni  37407  con1bii2  37644  con2bii2  37645  topdifinfeq  37662  isbasisrelowllem2  37668  wl-1xor  37794  wl-1mintru1  37800  wl-sb8eut  37894  wl-sb8eutv  37895  inixp  38040  notbinot1  38391  notbinot2  38395  truconj  38413  sbccom2lem  38436  sbccom2  38437  sbccom2f  38438  tsim1  38442  tsxo3  38451  tsxo4  38452  trcoss2  38886  dfcomember3  39071  eqvreldmqs  39072  eqvreldmqs2  39073  dfmembpart2  39185  eldisjn0el  39221  isopos  39617  islvol5  40016  elpadd0  40246  dvhopellsm  41554  diblsmopel  41608  mapdvalc  42066  3factsumint2  42453  3factsumint3  42454  3factsumint4  42455  aks4d1p1p2  42501  aks4d1p7  42514  isprimroot  42524  aks6d1c1p1  42538  aks6d1c2p2  42550  sticksstones22  42599  unitscyglem4  42629  elpwbi  42663  redvmptabs  42791  dffltz  43066  rmxypairf1o  43342  onsupmaxb  43670  ifpnotnotb  43909  ifpdfxor  43917  ifpidg  43921  ifpim123g  43930  ifpim1g  43931  ifpimimb  43934  ifpimim  43939  rp-fakeanorass  43943  elmapintrab  44006  undmrnresiss  44034  clcnvlem  44053  sqrtcvallem1  44061  cnviun  44080  dfxor4  44196  dfhe3  44205  dffrege69  44362  dffrege76  44369  or3or  44453  uneqsn  44455  scottabf  44670  mnurndlem1  44711  ismnushort  44731  pm10.252  44791  pm10.253  44792  pm10.42  44794  aaanv  44818  pm13.195  44843  pm13.196a  44844  sbc3or  44962  en3lpVD  45274  3orbi123VD  45279  sbc3orgVD  45280  sbcoreleleqVD  45288  undif3VD  45311  ax6e2ndeqVD  45338  ax6e2ndeqALT  45360  sineq0ALT  45366  n0abso  45406  permaxsep  45437  permaxinf2lem  45442  uzwo4  45487  iindif2f  45593  allbutfiinf  45852  limsupequzmptlem  46160  cncfshift  46306  dvnmul  46375  dvnprodlem2  46379  rrxsnicc  46732  salexct  46766  sge00  46808  sge0iunmpt  46850  meadjiun  46898  carageneld  46934  ovncvrrp  46996  ovolval4lem1  47081  vonioo  47114  vonicc  47117  nsssmfmbf  47211  smfmullem4  47226  aibandbiaiffaiffb  47328  plcofph  47378  pldofph  47379  plvcofph  47380  plvcofphax  47381  plvofpos  47382  n0nsn2el  47459  fsetsniunop  47483  2reu8i  47547  aovov0bi  47630  tz6.12-afv2  47674  4an21  47704  ichbi12i  47894  ichnfimlem  47897  spr0nelg  47910  sprvalpwn0  47917  reuprpr  47957  requad2  48057  clnbgrel  48262  usgrexmpl2nb4  48469  pg4cyclnex  48561  copisnmnd  48603  pgrpgt2nabl  48800  lindslinindsimp2lem5  48896  islininds2  48918  ldepslinc  48943  line2ylem  49185