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

Theorem bicomi 214
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 211 . 2 ((𝜑𝜓) → (𝜓𝜑))
31, 2ax-mp 5 1 (𝜓𝜑)
Colors of variables: wff setvar class
Syntax hints:  wb 196
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 197
This theorem is referenced by:  biimpri  218  bitr2i  265  bitr3i  266  bitr4i  267  syl5bbr  274  syl5rbbr  275  syl6bbr  278  syl6rbbr  279  mtbir  312  sylnibr  318  sylnbir  320  xchnxbir  322  xchbinxr  324  con1bii  345  con2bii  346  nbn  361  xor3  371  pm5.41  378  pm4.63  384  pm4.61  391  pm4.76  508  anidm  554  an43  637  anabs1  641  anabs7  643  pm4.87  832  pm4.64  838  pm4.25  891  pm4.77  947  anor  967  pm4.53  970  pm4.55  972  pm4.56  973  pm4.57  975  pm5.63  1005  3anor  1097  3ianorOLD  1098  3oran  1099  syl3anbr  1165  3an6  1557  nannot  1601  nanbi  1602  truan  1649  truimfal  1663  nottru  1666  falbitru  1669  nic-dfim  1742  nic-dfneg  1743  2nalexn  1903  2nexaln  1905  sbequ8  2054  equvinv  2115  equvelv  2118  cleljust  2153  cleljustALT  2347  cleljustALT2  2348  dvelimf  2484  sb5rf  2569  sb6rf  2570  sb10f  2604  abeq1i  2885  nne  2947  necon3bbii  2990  necon2abii  2993  necon2bbii  2994  nnel  3055  rspc2gv  3471  ceqsrexbv  3487  clel4  3493  rabeqc  3513  2reu5lem1  3565  2reu5lem2  3566  2reu5lem3  3567  dfsbcq2  3590  cbvreucsf  3716  nss  3812  dfdif3  3871  difab  4044  un0  4111  in0  4112  ss0b  4117  rexdifpr  4344  ssdifsnOLD  4455  ssunsn2  4493  iindif2  4723  nssss  5052  snopeqop  5098  epse  5232  restidsingOLD  5600  cotrg  5648  issref  5650  mptpreima  5772  ralrnmpt  6511  fmptsng  6578  fmptsnd  6579  dff14a  6670  f13dfv  6673  weniso  6747  abnex  7112  uniuni  7118  suppvalbr  7450  eroveu  7995  mapsnend  8188  isfinite2  8374  marypha1lem  8495  marypha2lem4  8500  infcllem  8549  wemapso2lem  8613  en3lplem2  8672  cantnfp1  8742  carden2  9013  fseqenlem1  9047  iscard3  9116  cardnum  9117  alephinit  9118  cardinfima  9120  alephiso  9121  dfac10b  9163  dfackm  9190  isfin5-2  9415  brdom7disj  9555  brdom6disj  9556  fsuppmapnn0fiubex  12999  hash2prb  13456  hashle2prv  13462  hashtpg  13469  wrd2ind  13686  splfv1  13715  cshwsexa  13779  s4f1o  13872  cotr2g  13925  relexpindlem  14011  lcmfunsnlem2  15561  ncoprmlnprm  15643  vdwapun  15885  cshwsiun  16013  cshwshash  16018  grpss  17648  pmtrfrn  18085  pmtrrn2  18087  pmtrprfvalrn  18115  issrg  18715  drngnidl  19444  drnglpir  19468  0ringnnzr  19484  unocv  20241  dsmmacl  20302  pmatcollpw2lem  20802  fvmptnn04if  20874  toptopon  20942  toprntopon  20950  ordtbas2  21216  ordtrest2  21229  xmeterval  22457  isclmp  23116  ovolfcl  23454  eldv  23882  eltayl  24334  musumsum  25139  umgrislfupgrlem  26238  numedglnl  26261  ausgrusgrb  26282  cplgr3v  26566  vtxd0nedgb  26619  finsumvtxdg2ssteplem1  26676  isrgr  26690  rgrusgrprc  26720  rgrprcx  26723  upgr2wlk  26799  pthsfval  26852  wlksnwwlknvbijOLD  27053  wwlksnwwlksnon  27060  usgr2wspthon  27114  isclwwlk  27134  clwwlkvbij  27289  clwwlkvbijOLDOLD  27290  clwwlkvbijOLD  27291  iseupthf1o  27382  frcond2  27449  nfrgr2v  27454  4cycl2vnunb  27472  fusgr2wsp2nb  27516  dlwwlknondlwlknonf1oOLD  27556  frgrregord013  27594  lejdii  28737  mdslle1i  29516  mdslle2i  29517  mdslj1i  29518  mdslj2i  29519  mo5f  29664  unipreima  29786  2ndpreima  29825  ordtrest2NEW  30309  ordtconnlem1  30310  ballotlem2  30890  plymulx0  30964  bnj115  31131  bnj156  31134  bnj206  31137  bnj110  31266  bnj121  31278  bnj124  31279  bnj130  31282  bnj153  31288  bnj207  31289  bnj581  31316  bnj611  31326  bnj864  31330  bnj865  31331  bnj893  31336  bnj1000  31349  bnj978  31357  bnj1040  31378  bnj1049  31380  bnj1133  31395  bnj1189  31415  cnvco1  31987  cnvco2  31988  dfiota3  32367  trer  32647  nabi1i  32728  nabi2i  32729  bj-dfifc2  32901  bj-df-ifc  32902  bj-dfssb2  32977  bj-hbext  33038  bj-dvelimdv  33168  bj-cleljustab  33181  bj-denotes  33187  bj-ralcom4  33197  bj-rexcom4  33198  bj-elsngl  33287  bj-nuliotaALT  33351  bj-rest10  33373  bj-restuni  33382  bj-ismooredr2  33397  con1bii2  33516  con2bii2  33517  topdifinfeq  33535  isbasisrelowllem2  33541  wl-sb8eut  33693  wl-clelv2-just  33712  inixp  33855  notbinot1  34210  notbinot2  34214  truconj  34235  sbccom2lem  34261  sbccom2  34262  sbccom2f  34263  tsim1  34269  tsxo3  34278  tsxo4  34279  trcoss2  34576  isopos  34989  islvol5  35387  elpadd0  35617  dvhopellsm  36927  diblsmopel  36981  mapdvalc  37439  rmxypairf1o  38002  acsfn1p  38295  ifpnotnotb  38350  ifpdfxor  38358  ifpidg  38362  ifpim123g  38371  ifpim1g  38372  ifpimimb  38375  ifpimim  38380  rp-fakeanorass  38384  rp-isfinite6  38390  elmapintrab  38408  undmrnresiss  38436  clcnvlem  38456  cnviun  38468  dfxor4  38584  dfhe3  38595  dffrege69  38752  dffrege76  38759  or3or  38845  uneqsn  38847  pm10.252  39086  pm10.253  39087  pm10.42  39089  aaanv  39114  pm13.195  39140  pm13.196a  39141  sbc3or  39263  sbc3orgOLD  39267  en3lpVD  39602  3orbi123VD  39607  sbc3orgVD  39608  undif3VD  39640  ax6e2ndeqVD  39667  ax6e2ndeqALT  39689  sineq0ALT  39695  uzwo4  39742  rnmptpr  39878  fompt  39899  allbutfiinf  40163  limsupequzmptlem  40478  cncfshift  40605  dvnmul  40676  dvnprodlem2  40680  rrxsnicc  41037  salexct  41069  sge00  41110  sge0iunmpt  41152  meadjiun  41200  carageneld  41236  ovncvrrp  41298  ovolval4lem1  41383  vonioo  41416  vonicc  41419  nsssmfmbf  41507  smfmullem4  41521  aibandbiaiffaiffb  41581  plcofph  41631  pldofph  41632  plvcofph  41633  plvcofphax  41634  plvofpos  41635  aovov0bi  41796  4an21  41810  spr0nelg  42254  sprvalpwn0  42261  copisnmnd  42337  pgrpgt2nabl  42675  lindslinindsimp2lem5  42779  islininds2  42801  ldepslinc  42826
  Copyright terms: Public domain W3C validator