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

Theorem bicomi 209
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 206 . 2 ((𝜑𝜓) → (𝜓𝜑))
31, 2ax-mp 5 1 (𝜓𝜑)
Colors of variables: wff setvar class
Syntax hints:  wb 191
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 192
This theorem is referenced by:  biimpri  213  bitr2i  260  bitr3i  261  bitr4i  262  syl5bbr  269  syl5rbbr  270  syl6bbr  273  syl6rbbr  274  mtbir  308  sylnibr  314  sylnbir  316  xchnxbir  318  xchbinxr  320  con1bii  340  con2bii  341  nbn  356  xor3  366  pm5.41  373  pm4.64  381  pm4.63  430  pm4.61  435  anor  503  pm4.53  506  pm4.55  508  pm4.56  509  pm4.57  511  pm4.25  530  pm4.87  600  anidm  665  pm4.77  814  anabs1  836  anabs7  838  an43  853  pm4.76  896  pm5.63  951  3ianor  1038  3oran  1040  pm3.2an3OLD  1224  syl3anbr  1352  3an6  1391  nannot  1434  nanbi  1435  nanbiOLD  1436  truan  1485  truimfal  1499  nottru  1502  falbitru  1505  nic-dfim  1582  nic-dfneg  1583  2nalexn  1731  2nexaln  1733  sbequ8  1833  cleljust  1945  cleljustALT  2135  cleljustALT2  2136  dvelimf  2217  sb5rf  2305  sb6rf  2306  sb10f  2339  abeq1i  2618  nne  2681  necon3bbii  2724  necon2abii  2727  necon2bbii  2728  nnel  2787  ceqsrexbv  3196  clel2  3198  clel4  3201  2reu5lem1  3269  2reu5lem2  3270  2reu5lem3  3271  dfsbcq2  3294  cbvreucsf  3419  nss  3512  raldifb  3598  difab  3738  un0  3797  in0  3798  ss0b  3803  ssunsn2  4161  rabasiun  4311  iindif2  4376  nssss  4697  opthneg  4722  epse  4863  restidsing  5211  cotrg  5261  issref  5263  mptpreima  5379  ralrnmpt  6098  fmptsng  6153  fmptsnd  6154  dff14a  6241  f13dfv  6244  weniso  6318  fvmptopab2  6408  uniuni  6677  suppvalbr  6997  eroveu  7540  isfinite2  7914  marypha1lem  8032  marypha2lem4  8037  infcllem  8086  wemapso2lem  8150  en3lplem2  8205  cantnfp1  8271  carden2  8506  fseqenlem1  8540  iscard3  8609  cardnum  8610  alephinit  8611  cardinfima  8613  alephiso  8614  dfac10b  8654  dfackm  8681  isfin5-2  8906  brdom7disj  9044  brdom6disj  9045  fsuppmapnn0fiubex  12318  hash2prb  12756  hashtpg  12764  wrd2ind  12967  splfv1  12995  cshwsexa  13059  s4f1o  13151  cotr2g  13198  relexpindlem  13286  lcmfunsnlem2  14775  ncoprmlnprm  14839  vdwapun  15086  cshwsiun  15231  cshwshash  15236  grpss  16847  pmtrfrn  17260  pmtrrn2  17262  pmtrprfvalrn  17290  issrg  17901  drngnidl  18612  drnglpir  18636  0ringnnzr  18652  unocv  19401  dsmmacl  19462  pmatcollpw2lem  19959  fvmptnn04if  20031  toptopon  20106  ordtbas2  20364  ordtrest2  20377  xmeterval  21605  ovolfcl  22578  eldv  23014  eltayl  23476  musumsum  24282  usgrafilem1  25300  trls  25427  is2wlk  25456  wwlknndef  25626  wlknwwlknvbij  25629  clwwlknndef  25662  clwwlkvbij  25690  el2wlkonotot0  25760  usg2spthonot0  25777  frgraun  25884  frgra2v  25887  4cycl2vnunb  25905  vdn0frgrav2  25911  vdgn0frgrav2  25912  2spotdisj  25949  usg2spot2nb  25953  usgreg2spot  25955  frgraregord013  26006  lejdii  27354  mdslle1i  28133  mdslle2i  28134  mdslj1i  28135  mdslj2i  28136  mo5f  28281  unipreima  28403  2ndpreima  28445  xrge0infssOLD  28497  ordtrest2NEW  28884  ordtconlem1  28885  ballotlem2  29475  plymulx0  29589  bnj115  29684  bnj156  29689  bnj206  29692  bnj110  29821  bnj121  29833  bnj124  29834  bnj130  29837  bnj153  29843  bnj207  29844  bnj581  29871  bnj611  29881  bnj864  29885  bnj865  29886  bnj893  29891  bnj1000  29904  bnj978  29912  bnj1040  29933  bnj1049  29935  bnj1133  29950  bnj1189  29970  cnvco1  30551  cnvco2  30552  dfiota3  30841  trer  31121  nabi1i  31201  nabi2i  31202  bj-dfifc2  31344  bj-df-ifc  31345  bj-nf3  31377  bj-dfssb2  31435  bj-hbext  31489  bj-denotes  31651  bj-ralcom4  31661  bj-rexcom4  31662  bj-elsngl  31748  bj-nuliotaALT  31810  bj-rest10  31821  bj-restuni  31830  bj-sspwpw  31837  bj-toprntopon  31843  con1bii2  31955  con2bii2  31956  topdifinfeq  31974  isbasisrelowllem2  31980  wl-sb8eut  32137  inixp  32293  notbinot1  32549  notbinot2  32553  truconj  32574  sbccom2lem  32600  sbccom2  32601  sbccom2f  32602  tsim1  32608  tsxo3  32617  tsxo4  32618  isopos  32986  islvol5  33384  elpadd0  33614  dvhopellsm  34925  diblsmopel  34979  mapdvalc  35437  rmxypairf1o  35999  acsfn1p  36305  ifpnotnotb  36363  ifpdfxor  36371  ifpidg  36375  ifpim123g  36384  ifpim1g  36385  ifpimimb  36388  ifpimim  36393  rp-fakeanorass  36397  rp-isfinite6  36403  elmapintrab  36421  undmrnresiss  36449  clcnvlem  36469  cnviun  36481  dfxor4  36597  dfhe3  36609  dffrege69  36767  dffrege76  36774  pm10.252  37067  pm10.253  37068  pm10.42  37070  aaanv  37095  pm13.195  37121  pm13.196a  37122  sbc3or  37245  sbc3orgOLD  37249  en3lpVD  37589  3orbi123VD  37594  sbc3orgVD  37595  undif3VD  37627  ax6e2ndeqVD  37654  ax6e2ndeqALT  37676  sineq0ALT  37682  uzwo4  37735  inn0f  37758  rnmptpr  37805  fompt  37827  mapsnend  37839  cncfshift  38160  dvnmul  38237  dvnprodlem2  38241  rrxsnicc  38605  salexct  38637  sge00  38664  sge0iunmpt  38706  meadjiun  38754  carageneld  38787  ovncvrrp  38849  ovolval4lem1  38934  vonioo  38968  vonicc  38971  aibandbiaiffaiffb  39002  plcofph  39052  pldofph  39053  plvcofph  39054  plvcofphax  39055  plvofpos  39056  aovov0bi  39218  rexdifpr  39516  umgrislfupgrlem  39747  ausgrusgrb  39795  cplgr3v  40057  vtxd0nedgb  40103  isrgr  40159  rgrusgrprc  40189  rgrprcx  40192  upgr2wlk  40276  wlksnwwlknvbij  40514  usgr2wspthon  40568  isclwwlks  40588  clwwlksvbij  40629  frcond2  40839  nfrgr2v  40842  4cycl2vnunb-av  40860  fusgr2wsp2nb  40898  av-frgraregord013  40949  copisnmnd  40999  pgrpgt2nabl  41341  lindslinindsimp2lem5  41445  islininds2  41467  ldepslinc  41492
  Copyright terms: Public domain W3C validator