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 ⊢ (𝜓 ↔ 𝜑)

Syntax hints:   ↔ wb 209

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 210

This theorem is referenced by:  biimpri  231  bitr2i  279  bitr3i  280  bitr4i  281  bitr3id  288  bitr3di  289  syl6bbr  292  bitr4id  293  mtbir  326  sylnibr  332  sylnbir  334  xchnxbir  336  xchbinxr  338  con1bii  360  nbn  376  xor3  387  pm5.41  395  pm4.63  401  pm4.61  408  pm4.76  522  anidm  568  an21  643  an43  657  anabs1  661  anabs7  663  pm4.87  840  pm4.64  846  pm4.25  903  pm4.77  960  pm4.53  983  pm4.55  985  pm4.56  986  pm4.57  988  pm5.63  1017  3anor  1105  3oran  1106  syl3anbr  1159  3an6  1443  nanbi  1491  nornot  1525  nororOLD  1530  truan  1549  truimfal  1562  nottru  1565  falbitru  1568  falnorfalOLD  1593  nic-dfim  1671  nic-dfneg  1672  2nalexn  1829  2nexaln  1831  equvinv  2036  cleljust  2120  sbelx  2252  sb5  2273  dfsb7OLD  2282  sb6rfv  2365  cleljustALT  2371  cleljustALT2  2372  dvelimf  2459  sb5rf  2479  sb6rf  2480  sb10f  2547  nexmo  2599  exists2  2724  cleljustab  2779  abeq1i  2926  abbi2dv  2927  nfabdw  2976  nne  2991  necon3bbii  3034  necon2abii  3037  necon2bbii  3038  nnel  3100  ralcom4  3198  rexcom4  3212  nelb  3227  rspc2gv  3580  ceqsrexbv  3598  clel4  3604  rabeqc  3626  2reu5lem1  3694  2reu5lem2  3695  2reu5lem3  3696  dfsbcq2  3723  cbvreucsf  3872  nss  3977  ss2abdv  3991  dfdif3  4042  symdifass  4178  difab  4224  neq0  4259  un0  4298  in0  4299  ss0b  4305  2nreu  4349  rexdifpr  4558  reuprg  4599  ssunsn2  4720  iindif2  4962  nssss  5313  snopeqop  5361  epse  5502  rnep  5761  cotrg  5938  mptpreima  6059  ralrnmpt  6839  fmptsng  6907  fmptsnd  6908  dff14a  7006  f13dfv  7009  weniso  7086  abnex  7459  uniuni  7464  suppvalbr  7817  eroveu  8375  mapsnend  8571  isfinite2  8760  marypha1lem  8881  marypha2lem4  8886  infcllem  8935  en3lplem2  9060  cantnfp1  9128  carden2  9400  fseqenlem1  9435  iscard3  9504  cardnum  9505  alephinit  9506  cardinfima  9508  alephiso  9509  dfac10b  9550  dfackm  9577  isfin5-2  9802  brdom7disj  9942  brdom6disj  9943  fsuppmapnn0fiubex  13355  hash2prb  13826  hashle2prv  13832  hashtpg  13839  swrdnnn0nd  14009  wrd2ind  14076  cshwsexa  14177  s4f1o  14271  cotr2g  14327  relexpindlem  14414  lcmfunsnlem2  15974  ncoprmlnprm  16058  vdwapun  16300  cshwsiun  16425  cshwshash  16430  grpss  18113  symgsubmefmnd  18518  pmtrfrn  18578  pmtrrn2  18580  pmtrprfvalrn  18608  issrg  19250  acsfn1p  19571  0ringnnzr  20035  unocv  20369  dsmmacl  20430  pmatcollpw2lem  21382  fvmptnn04if  21454  toptopon  21522  ordtbas2  21796  ordtrest2  21809  xmeterval  23039  isclmp  23702  ovolfcl  24070  eldv  24501  eltayl  24955  musumsum  25777  2sqreu  26040  2sqreunn  26041  2sqreult  26042  2sqreultb  26043  2sqreunnlt  26044  2sqreunnltb  26045  umgrislfupgrlem  26915  numedglnl  26937  ausgrusgrb  26958  cplgr3v  27225  vtxd0nedgb  27278  finsumvtxdg2ssteplem1  27335  isrgr  27349  rgrusgrprc  27379  rgrprcx  27382  upgr2wlk  27458  pthsfval  27510  wwlksnwwlksnon  27701  usgr2wspthon  27751  isclwwlk  27769  clwwlkvbij  27898  iseupthf1o  27987  frcond2  28052  nfrgr2v  28057  4cycl2vnunb  28075  fusgr2wsp2nb  28119  frgrregord013  28180  lejdii  29321  mdslle1i  30100  mdslle2i  30101  mdslj1i  30102  mdslj2i  30103  mo5f  30260  unipreima  30405  2ndpreima  30467  mcgcnv  30705  ordtrest2NEW  31276  ordtconnlem1  31277  ballotlem2  31856  plymulx0  31927  bnj115  32105  bnj156  32108  bnj206  32111  bnj110  32240  bnj121  32252  bnj124  32253  bnj130  32256  bnj153  32262  bnj207  32263  bnj581  32290  bnj611  32300  bnj864  32304  bnj865  32305  bnj893  32310  bnj1000  32323  bnj978  32331  bnj1040  32354  bnj1049  32356  bnj1133  32371  bnj1189  32391  satfv1  32723  satfvsucsuc  32725  satfdm  32729  satf0  32732  satf0op  32737  fmlafvel  32745  cnvco1  33108  cnvco2  33109  dfiota3  33497  trer  33777  nabi1i  33855  nabi2i  33856  bj-hbext  34157  bj-nnfbit  34196  bj-dvelimdv  34290  bj-elsngl  34404  bj-nuliotaALT  34475  bj-rest10  34503  bj-restuni  34512  con1bii2  34749  con2bii2  34750  topdifinfeq  34767  isbasisrelowllem2  34773  wl-1xor  34899  wl-1mintru1  34905  wl-sb8eut  34978  wl-dfralf  35004  inixp  35166  notbinot1  35517  notbinot2  35521  truconj  35539  sbccom2lem  35562  sbccom2  35563  sbccom2f  35564  tsim1  35568  tsxo3  35577  tsxo4  35578  trcoss2  35884  dfmember3  36068  eqvreldmqs  36069  isopos  36476  islvol5  36875  elpadd0  37105  dvhopellsm  38413  diblsmopel  38467  mapdvalc  38925  3factsumint2  39310  3factsumint3  39311  3factsumint4  39312  elpwbi  39410  dffltz  39615  rmxypairf1o  39852  ifpnotnotb  40187  ifpdfxor  40195  ifpidg  40199  ifpim123g  40208  ifpim1g  40209  ifpimimb  40212  ifpimim  40217  rp-fakeanorass  40221  elmapintrab  40276  undmrnresiss  40304  clcnvlem  40323  sqrtcvallem1  40331  cnviun  40351  dfxor4  40467  dfhe3  40476  dffrege69  40633  dffrege76  40640  or3or  40724  uneqsn  40726  scottabf  40948  mnurndlem1  40989  pm10.252  41065  pm10.253  41066  pm10.42  41068  aaanv  41092  pm13.195  41117  pm13.196a  41118  sbc3or  41238  en3lpVD  41551  3orbi123VD  41556  sbc3orgVD  41557  sbcoreleleqVD  41565  undif3VD  41588  ax6e2ndeqVD  41615  ax6e2ndeqALT  41637  sineq0ALT  41643  uzwo4  41687  fompt  41819  allbutfiinf  42057  limsupequzmptlem  42370  cncfshift  42516  dvnmul  42585  dvnprodlem2  42589  rrxsnicc  42942  salexct  42974  sge00  43015  sge0iunmpt  43057  meadjiun  43105  carageneld  43141  ovncvrrp  43203  ovolval4lem1  43288  vonioo  43321  vonicc  43324  nsssmfmbf  43412  smfmullem4  43426  aibandbiaiffaiffb  43487  plcofph  43537  pldofph  43538  plvcofph  43539  plvcofphax  43540  plvofpos  43541  2reu8i  43669  aovov0bi  43752  tz6.12-afv2  43796  4an21  43826  ichbi12i  43977  ichnfimlem  43980  spr0nelg  43993  sprvalpwn0  44000  reuprpr  44040  requad2  44141  copisnmnd  44429  pgrpgt2nabl  44768  lindslinindsimp2lem5  44871  islininds2  44893  ldepslinc  44918  line2ylem  45165