Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  bicomi Structured version   Visualization version   GIF version

Theorem bicomi 225
 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
StepHypRef Expression
1 bicomi.1 . 2 (𝜑𝜓)
2 bicom1 222 . 2 ((𝜑𝜓) → (𝜓𝜑))
31, 2ax-mp 5 1 (𝜓𝜑)
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 207 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 208 This theorem is referenced by:  biimpri  229  bitr2i  277  bitr3i  278  bitr4i  279  syl5bbr  286  syl5rbbr  287  syl6bbr  290  syl6rbbr  291  mtbir  324  sylnibr  330  sylnbir  332  xchnxbir  334  xchbinxr  336  con1bii  358  nbn  374  xor3  384  pm5.41  392  pm4.63  398  pm4.61  405  pm4.76  519  anidm  565  an21  640  an43  654  anabs1  658  anabs7  660  pm4.87  839  pm4.64  845  pm4.25  901  pm4.77  958  pm4.53  981  pm4.55  983  pm4.56  984  pm4.57  986  pm5.63  1015  3anor  1102  3oran  1103  syl3anbr  1156  3an6  1439  nanbi  1486  nornot  1517  nororOLD  1522  truan  1541  truimfal  1554  nottru  1557  falbitru  1560  falnorfalOLD  1585  nic-dfim  1663  nic-dfneg  1664  2nalexn  1821  2nexaln  1823  equvinv  2029  cleljust  2115  sbelx  2246  sb5  2268  dfsb7OLD  2280  sb6rfv  2371  cleljustALT  2377  cleljustALT2  2378  dvelimf  2467  sb5rf  2487  sb6rf  2488  sb10f  2564  nexmo  2616  exists2  2747  cleljustab  2805  abeq1i  2953  abbi2dv  2954  nfabdw  3004  nne  3024  necon3bbii  3067  necon2abii  3070  necon2bbii  3071  nnel  3136  ralcom4  3239  rexcom4  3253  nelb  3272  rspc2gv  3635  ceqsrexbv  3653  clel4  3659  rabeqc  3681  2reu5lem1  3749  2reu5lem2  3750  2reu5lem3  3751  dfsbcq2  3778  cbvreucsf  3930  nss  4032  dfdif3  4094  symdifass  4231  difab  4275  un0  4347  in0  4348  ss0b  4354  2nreu  4395  rexdifpr  4594  reuprg  4637  ssunsn2  4758  iindif2  4995  nssss  5344  snopeqop  5392  epse  5536  rnep  5795  cotrg  5968  mptpreima  6089  ralrnmpt  6857  fmptsng  6925  fmptsnd  6926  dff14a  7025  f13dfv  7028  weniso  7102  abnex  7471  uniuni  7476  suppvalbr  7828  eroveu  8385  mapsnend  8580  isfinite2  8768  marypha1lem  8889  marypha2lem4  8894  infcllem  8943  en3lplem2  9068  cantnfp1  9136  carden2  9408  fseqenlem1  9442  iscard3  9511  cardnum  9512  alephinit  9513  cardinfima  9515  alephiso  9516  dfac10b  9557  dfackm  9584  isfin5-2  9805  brdom7disj  9945  brdom6disj  9946  fsuppmapnn0fiubex  13353  hash2prb  13823  hashle2prv  13829  hashtpg  13836  swrdnnn0nd  14011  wrd2ind  14078  cshwsexa  14179  s4f1o  14273  cotr2g  14329  relexpindlem  14415  lcmfunsnlem2  15976  ncoprmlnprm  16060  vdwapun  16302  cshwsiun  16425  cshwshash  16430  grpss  18053  pmtrfrn  18508  pmtrrn2  18510  pmtrprfvalrn  18538  issrg  19179  acsfn1p  19500  0ringnnzr  19963  unocv  20740  dsmmacl  20801  pmatcollpw2lem  21301  fvmptnn04if  21373  toptopon  21441  ordtbas2  21715  ordtrest2  21728  xmeterval  22957  isclmp  23616  ovolfcl  23982  eldv  24411  eltayl  24863  musumsum  25683  2sqreu  25946  2sqreunn  25947  2sqreult  25948  2sqreultb  25949  2sqreunnlt  25950  2sqreunnltb  25951  umgrislfupgrlem  26822  numedglnl  26844  ausgrusgrb  26865  cplgr3v  27132  vtxd0nedgb  27185  finsumvtxdg2ssteplem1  27242  isrgr  27256  rgrusgrprc  27286  rgrprcx  27289  upgr2wlk  27365  pthsfval  27417  wwlksnwwlksnon  27609  usgr2wspthon  27659  isclwwlk  27677  clwwlkvbij  27807  iseupthf1o  27896  frcond2  27961  nfrgr2v  27966  4cycl2vnunb  27984  fusgr2wsp2nb  28028  frgrregord013  28089  lejdii  29230  mdslle1i  30009  mdslle2i  30010  mdslj1i  30011  mdslj2i  30012  mo5f  30168  unipreima  30307  2ndpreima  30357  ordtrest2NEW  31053  ordtconnlem1  31054  ballotlem2  31633  plymulx0  31704  bnj115  31882  bnj156  31885  bnj206  31888  bnj110  32017  bnj121  32029  bnj124  32030  bnj130  32033  bnj153  32039  bnj207  32040  bnj581  32067  bnj611  32077  bnj864  32081  bnj865  32082  bnj893  32087  bnj1000  32100  bnj978  32108  bnj1040  32129  bnj1049  32131  bnj1133  32146  bnj1189  32166  satfv1  32495  satfvsucsuc  32497  satfdm  32501  satf0  32504  satf0op  32509  fmlafvel  32517  cnvco1  32880  cnvco2  32881  dfiota3  33269  trer  33549  nabi1i  33627  nabi2i  33628  bj-hbext  33929  bj-nnfbit  33966  bj-dvelimdv  34060  bj-denotes  34073  bj-elsngl  34165  bj-nuliotaALT  34233  bj-rest10  34261  bj-restuni  34270  con1bii2  34483  con2bii2  34484  topdifinfeq  34501  isbasisrelowllem2  34507  wl-sb8eut  34681  wl-dfralf  34707  inixp  34872  notbinot1  35226  notbinot2  35230  truconj  35248  sbccom2lem  35271  sbccom2  35272  sbccom2f  35273  tsim1  35277  tsxo3  35286  tsxo4  35287  trcoss2  35592  dfmember3  35776  eqvreldmqs  35777  isopos  36184  islvol5  36583  elpadd0  36813  dvhopellsm  38121  diblsmopel  38175  mapdvalc  38633  elpwbi  38982  dffltz  39133  rmxypairf1o  39370  ifpnotnotb  39707  ifpdfxor  39715  ifpidg  39719  ifpim123g  39728  ifpim1g  39729  ifpimimb  39732  ifpimim  39737  rp-fakeanorass  39741  elmapintrab  39798  undmrnresiss  39826  clcnvlem  39845  cnviun  39857  dfxor4  39973  dfhe3  39983  dffrege69  40140  dffrege76  40147  or3or  40233  uneqsn  40235  scottabf  40438  mnurndlem1  40479  pm10.252  40555  pm10.253  40556  pm10.42  40558  aaanv  40582  pm13.195  40607  pm13.196a  40608  sbc3or  40728  en3lpVD  41041  3orbi123VD  41046  sbc3orgVD  41047  sbcoreleleqVD  41055  undif3VD  41078  ax6e2ndeqVD  41105  ax6e2ndeqALT  41127  sineq0ALT  41133  uzwo4  41177  fompt  41315  allbutfiinf  41556  limsupequzmptlem  41871  cncfshift  42019  dvnmul  42090  dvnprodlem2  42094  rrxsnicc  42448  salexct  42480  sge00  42521  sge0iunmpt  42563  meadjiun  42611  carageneld  42647  ovncvrrp  42709  ovolval4lem1  42794  vonioo  42827  vonicc  42830  nsssmfmbf  42918  smfmullem4  42932  aibandbiaiffaiffb  42993  plcofph  43043  pldofph  43044  plvcofph  43045  plvcofphax  43046  plvofpos  43047  2reu8i  43175  aovov0bi  43258  tz6.12-afv2  43302  4an21  43332  dfich2ai  43443  ichbi12i  43447  spr0nelg  43467  sprvalpwn0  43474  reuprpr  43514  requad2  43617  copisnmnd  43905  pgrpgt2nabl  44243  lindslinindsimp2lem5  44346  islininds2  44368  ldepslinc  44393  line2ylem  44567
 Copyright terms: Public domain W3C validator