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

Theorem bicomi 212
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 209 . 2 ((𝜑𝜓) → (𝜓𝜑))
31, 2ax-mp 5 1 (𝜓𝜑)
Colors of variables: wff setvar class
Syntax hints:  wb 194
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 195
This theorem is referenced by:  biimpri  216  bitr2i  263  bitr3i  264  bitr4i  265  syl5bbr  272  syl5rbbr  273  syl6bbr  276  syl6rbbr  277  mtbir  311  sylnibr  317  sylnbir  319  xchnxbir  321  xchbinxr  323  con1bii  344  con2bii  345  nbn  360  xor3  370  pm5.41  377  pm4.64  385  pm4.63  435  pm4.61  440  anor  508  pm4.53  511  pm4.55  513  pm4.56  514  pm4.57  516  pm4.25  535  pm4.87  605  anidm  673  pm4.77  823  anabs1  845  anabs7  847  an43  862  pm4.76  905  pm5.63  960  3ianor  1047  3oran  1049  pm3.2an3OLD  1233  syl3anbr  1361  3an6  1400  nannot  1444  nanbi  1445  truan  1491  truimfal  1505  nottru  1508  falbitru  1511  nic-dfim  1584  nic-dfneg  1585  2nalexn  1733  2nexaln  1735  sbequ8  1835  cleljust  1946  cleljustALT  2134  cleljustALT2  2135  dvelimf  2226  sb5rf  2314  sb6rf  2315  sb10f  2348  abeq1i  2627  nne  2690  necon3bbii  2733  necon2abii  2736  necon2bbii  2737  nnel  2796  ceqsrexbv  3211  clel2  3213  clel4  3216  2reu5lem1  3284  2reu5lem2  3285  2reu5lem3  3286  dfsbcq2  3309  cbvreucsf  3437  nss  3530  difab  3758  un0  3822  in0  3823  ss0b  3828  ssunsn2  4200  iindif2  4423  nssss  4749  epse  4915  restidsingOLD  5268  cotrg  5317  issref  5319  mptpreima  5435  ralrnmpt  6159  fmptsng  6215  fmptsnd  6216  dff14a  6303  f13dfv  6306  weniso  6380  fvmptopab2  6471  uniuni  6740  suppvalbr  7060  eroveu  7604  isfinite2  7978  marypha1lem  8097  marypha2lem4  8102  infcllem  8151  wemapso2lem  8215  en3lplem2  8270  cantnfp1  8336  carden2  8571  fseqenlem1  8605  iscard3  8674  cardnum  8675  alephinit  8676  cardinfima  8678  alephiso  8679  dfac10b  8719  dfackm  8746  isfin5-2  8971  brdom7disj  9109  brdom6disj  9110  fsuppmapnn0fiubex  12521  hash2prb  12974  hashtpg  12982  wrd2ind  13186  splfv1  13214  cshwsexa  13278  s4f1o  13370  cotr2g  13420  relexpindlem  13508  lcmfunsnlem2  15065  ncoprmlnprm  15148  vdwapun  15398  cshwsiun  15526  cshwshash  15531  grpss  17153  pmtrfrn  17591  pmtrrn2  17593  pmtrprfvalrn  17621  issrg  18235  drngnidl  18952  drnglpir  18976  0ringnnzr  18992  unocv  19744  dsmmacl  19805  pmatcollpw2lem  20302  fvmptnn04if  20374  toptopon  20449  ordtbas2  20706  ordtrest2  20719  xmeterval  21947  ovolfcl  22918  eldv  23344  eltayl  23806  musumsum  24608  usgrafilem1  25679  trls  25805  is2wlk  25834  wwlknndef  26004  wlknwwlknvbij  26007  clwwlknndef  26040  clwwlkvbij  26068  el2wlkonotot0  26138  usg2spthonot0  26155  frgraun  26262  frgra2v  26265  4cycl2vnunb  26283  vdn0frgrav2  26289  vdgn0frgrav2  26290  2spotdisj  26327  usg2spot2nb  26331  usgreg2spot  26333  frgraregord013  26384  lejdii  27570  mdslle1i  28349  mdslle2i  28350  mdslj1i  28351  mdslj2i  28352  mo5f  28497  unipreima  28615  2ndpreima  28657  xrge0infssOLD  28707  ordtrest2NEW  29094  ordtconlem1  29095  ballotlem2  29685  plymulx0  29796  bnj115  29891  bnj156  29896  bnj206  29899  bnj110  30028  bnj121  30040  bnj124  30041  bnj130  30044  bnj153  30050  bnj207  30051  bnj581  30078  bnj611  30088  bnj864  30092  bnj865  30093  bnj893  30098  bnj1000  30111  bnj978  30119  bnj1040  30140  bnj1049  30142  bnj1133  30157  bnj1189  30177  cnvco1  30746  cnvco2  30747  dfiota3  31036  trer  31316  nabi1i  31396  nabi2i  31397  bj-dfifc2  31569  bj-df-ifc  31570  bj-nf3  31602  bj-dfssb2  31664  bj-hbext  31723  bj-denotes  31884  bj-ralcom4  31894  bj-rexcom4  31895  bj-elsngl  31981  bj-nuliotaALT  32043  bj-rest10  32054  bj-restuni  32063  bj-sspwpw  32070  bj-toprntopon  32076  con1bii2  32187  con2bii2  32188  topdifinfeq  32206  isbasisrelowllem2  32212  wl-nf4  32298  wl-sb8eut  32413  inixp  32568  notbinot1  32923  notbinot2  32927  truconj  32948  sbccom2lem  32974  sbccom2  32975  sbccom2f  32976  tsim1  32982  tsxo3  32991  tsxo4  32992  isopos  33360  islvol5  33758  elpadd0  33988  dvhopellsm  35299  diblsmopel  35353  mapdvalc  35811  rmxypairf1o  36369  acsfn1p  36670  ifpnotnotb  36725  ifpdfxor  36733  ifpidg  36737  ifpim123g  36746  ifpim1g  36747  ifpimimb  36750  ifpimim  36755  rp-fakeanorass  36759  rp-isfinite6  36765  elmapintrab  36783  undmrnresiss  36811  clcnvlem  36831  cnviun  36843  dfxor4  36959  dfhe3  36971  dffrege69  37128  dffrege76  37135  or3or  37221  uneqsn  37223  pm10.252  37464  pm10.253  37465  pm10.42  37467  aaanv  37492  pm13.195  37518  pm13.196a  37519  sbc3or  37641  sbc3orgOLD  37645  en3lpVD  37984  3orbi123VD  37989  sbc3orgVD  37990  undif3VD  38022  ax6e2ndeqVD  38049  ax6e2ndeqALT  38071  sineq0ALT  38077  uzwo4  38129  inn0f  38151  rnmptpr  38236  fompt  38258  mapsnend  38270  cncfshift  38646  dvnmul  38723  dvnprodlem2  38727  rrxsnicc  39090  salexct  39122  sge00  39163  sge0iunmpt  39205  meadjiun  39253  carageneld  39286  ovncvrrp  39348  ovolval4lem1  39433  vonioo  39467  vonicc  39470  nsssmfmbf  39559  smfmullem4  39573  aibandbiaiffaiffb  39604  plcofph  39654  pldofph  39655  plvcofph  39656  plvcofphax  39657  plvofpos  39658  aovov0bi  39820  rexdifpr  40211  umgrislfupgrlem  40439  ausgrusgrb  40487  cplgr3v  40749  vtxd0nedgb  40795  isrgr  40851  rgrusgrprc  40881  rgrprcx  40884  upgr2wlk  40968  wlksnwwlknvbij  41206  usgr2wspthon  41260  isclwwlks  41280  clwwlksvbij  41321  frcond2  41531  nfrgr2v  41534  4cycl2vnunb-av  41552  fusgr2wsp2nb  41590  av-frgraregord013  41641  copisnmnd  41691  pgrpgt2nabl  42033  lindslinindsimp2lem5  42137  islininds2  42159  ldepslinc  42184
  Copyright terms: Public domain W3C validator