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  bitr3id  287  bitr3di  288  bitr4di  291  bitr4id  292  mtbir  325  sylnibr  331  sylnbir  333  xchnxbir  335  xchbinxr  337  con1bii  358  nbn  374  xor3  384  pm5.41  393  pm4.63  401  pm4.61  408  pm4.76  526  anidm  572  an21  654  an43  668  anabs1  672  anabs7  674  pm4.87  854  pm4.64  860  pm4.25  916  pm4.77  975  pm4.53  999  pm4.55  1001  pm4.56  1002  pm4.57  1004  pm5.63  1033  3anor  1121  3oran  1122  syl3anbr  1176  3an6  1469  nanbi  1522  nornot  1553  truan  1573  truimfal  1586  nottru  1589  falbitru  1592  nic-dfim  1691  nic-dfneg  1692  2nalexn  1850  2nexaln  1852  equvinv  2051  cleljust  2153  sbelx  2290  sb6rfv  2390  cleljustALT  2397  cleljustALT2  2398  dvelimf  2481  sb5rf  2500  sb6rf  2501  sb10f  2560  nexmo  2570  exists2  2690  cleljustab  2745  eqabdv  2897  eqabcri  2907  nne  2963  necon3bbii  3006  necon2abii  3009  necon2bbii  3010  nnel  3073  r19.41v  3194  r3ex  3203  r19.41  3268  rspc2gv  3593  ceqsrexbv  3617  2reu5lem1  3720  2reu5lem2  3721  2reu5lem3  3722  dfsbcq2  3749  cbvreucsf  3898  nss  4002  dfdif3OLD  4074  symdifass  4216  indifdi  4248  difab  4264  neq0  4306  un0  4350  in0  4351  ss0b  4357  2nreu  4400  ralidm  4473  reuprg  4664  snssb  4743  snssg  4744  ssunsn2  4787  iindif2  5036  eqsnuniex  5320  nssss  5424  snopeqop  5477  dffr6  5605  epse  5631  rnep  5905  mptpreima  6227  ralrnmpt  7079  fmptsng  7154  fmptsnd  7155  dff14a  7256  f13dfv  7260  weniso  7340  abnex  7742  uniuni  7747  frpoins3xp3g  8123  xpord3inddlem  8136  eroveu  8796  fsetexb  8847  mapsnend  9019  isfinite2  9244  marypha1lem  9381  marypha2lem4  9386  infcllem  9436  en3lplem2  9570  cantnfp1  9638  carden2  9947  fseqenlem1  9982  iscard3  10051  cardnum  10052  alephinit  10053  cardinfima  10055  alephiso  10056  dfac10b  10098  dfackm  10125  isfin5-2  10350  brdom7disj  10490  brdom6disj  10491  fsuppmapnn0fiubex  14007  hash2prb  14487  hashle2prv  14493  hashtpg  14500  hash3tpb  14510  swrdnnn0nd  14672  wrd2ind  14738  s4f1o  14933  cotr2g  14991  relexpindlem  15078  lcmfunsnlem2  16676  ncoprmlnprm  16765  vdwapun  17012  cshwsiun  17137  cshwshash  17142  grpss  18998  symgsubmefmnd  19440  pmtrfrn  19500  pmtrrn2  19502  pmtrprfvalrn  19530  issrg  20240  0ringnnzr  20577  acsfn1p  20850  unocv  21734  dsmmacl  21795  pmatcollpw2lem  22839  fvmptnn04if  22911  toptopon  22979  ordtbas2  23253  ordtrest2  23266  xmeterval  24494  isclmp  25161  ovolfcl  25530  eldv  25962  plyn0mulidp  26347  eltayl  26425  musumsum  27258  2sqreu  27522  2sqreunn  27523  2sqreult  27524  2sqreultb  27525  2sqreunnlt  27526  2sqreunnltb  27527  nosupinfsep  27798  umgrislfupgrlem  29325  numedglnl  29347  ausgrusgrb  29368  cplgr3v  29638  vtxd0nedgb  29691  finsumvtxdg2ssteplem1  29748  isrgr  29762  rgrusgrprc  29792  rgrprcx  29795  upgr2wlk  29869  dfpth2  29931  wwlksnwwlksnon  30117  usgr2wspthon  30170  isclwwlk  30188  clwwlkvbij  30317  iseupthf1o  30406  frcond2  30471  nfrgr2v  30476  4cycl2vnunb  30494  fusgr2wsp2nb  30538  frgrregord013  30599  lejdii  31743  mdslle1i  32522  mdslle2i  32523  mdslj1i  32524  mdslj2i  32525  mo5f  32690  n0nsnel  32716  unipreima  32847  2ndpreima  32912  mgccnv  33179  domnprodeq0  33462  quslsm  33593  mplmonprod  33853  ordtrest2NEW  34222  ordtconnlem1  34223  ballotlem2  34788  bnj115  35023  bnj156  35026  bnj206  35029  bnj110  35155  bnj121  35167  bnj124  35168  bnj130  35171  bnj153  35177  bnj207  35178  bnj581  35205  bnj611  35215  bnj864  35219  bnj865  35220  bnj893  35225  bnj1000  35238  bnj978  35246  bnj1040  35269  bnj1049  35271  bnj1133  35286  bnj1189  35306  satfv1  35718  satfvsucsuc  35720  satfdm  35724  satf0  35727  satf0op  35732  fmlafvel  35740  cnvco1  36114  cnvco2  36115  dfiota3  36276  ss-ax8  36590  trer  36681  nabi1i  36759  nabi2i  36760  regsfromregtco  36903  bj-nnfbit  37238  bj-dvelimdv  37341  bj-gabima  37430  bj-elsngl  37458  bj-nuliotaALT  37548  bj-axseprep  37564  bj-rest10  37583  bj-restuni  37592  con1bii2  37831  con2bii2  37832  topdifinfeq  37849  isbasisrelowllem2  37855  wl-1xor  37981  wl-1mintru1  37987  wl-sb8eut  38086  wl-sb8eutv  38087  inixp  38232  notbinot1  38583  notbinot2  38587  truconj  38605  sbccom2lem  38628  sbccom2  38629  sbccom2f  38630  tsim1  38634  tsxo3  38643  tsxo4  38644  trcoss2  39078  dfcomember3  39263  eqvreldmqs  39264  eqvreldmqs2  39265  dfmembpart2  39377  eldisjn0el  39413  isopos  39809  islvol5  40208  elpadd0  40438  dvhopellsm  41746  diblsmopel  41800  mapdvalc  42258  3factsumint2  42644  3factsumint3  42645  3factsumint4  42646  aks4d1p1p2  42692  aks4d1p7  42705  isprimroot  42715  aks6d1c1p1  42729  aks6d1c2p2  42741  sticksstones22  42790  unitscyglem4  42820  elpwbi  42854  redvmptabs  42974  dffltz  43221  rmxypairf1o  43493  onsupmaxb  43821  ifpnotnotb  44060  ifpdfxor  44068  ifpidg  44072  ifpim123g  44081  ifpim1g  44082  ifpimimb  44085  ifpimim  44090  rp-fakeanorass  44094  elmapintrab  44157  undmrnresiss  44185  clcnvlem  44204  sqrtcvallem1  44212  cnviun  44231  dfxor4  44347  dfhe3  44356  dffrege69  44513  dffrege76  44520  or3or  44604  uneqsn  44606  scottabf  44821  mnurndlem1  44862  ismnushort  44882  pm10.252  44942  pm10.253  44943  pm10.42  44945  aaanv  44969  pm13.195  44994  pm13.196a  44995  sbc3or  45113  en3lpVD  45425  3orbi123VD  45430  sbc3orgVD  45431  sbcoreleleqVD  45439  undif3VD  45462  ax6e2ndeqVD  45489  ax6e2ndeqALT  45511  sineq0ALT  45517  n0abso  45557  permaxsep  45588  permaxinf2lem  45593  iindif2f  45743  allbutfiinf  45999  limsupequzmptlem  46307  cncfshift  46453  dvnmul  46522  dvnprodlem2  46526  rrxsnicc  46879  sge00  46955  sge0iunmpt  46997  meadjiun  47045  ovolval4lem1  47228  nsssmfmbf  47358  smfmullem4  47373  aibandbiaiffaiffb  47493  plcofph  47543  pldofph  47544  plvcofph  47545  plvcofphax  47546  plvofpos  47547  n0nsn2el  47624  fsetsniunop  47648  2reu8i  47712  aovov0bi  47795  tz6.12-afv2  47839  4an21  47869  ichbi12i  48071  ichnfimlem  48074  spr0nelg  48087  sprvalpwn0  48094  reuprpr  48134  nprmmul1  48138  requad2  48250  clnbgrel  48455  usgrexmpl2nb4  48662  pg4cyclnex  48754  copisnmnd  48796  pgrpgt2nabl  48993  lindslinindsimp2lem5  49089  islininds2  49111  ldepslinc  49136  line2ylem  49378