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  313  sylnibr  319  sylnbir  321  xchnxbir  323  xchbinxr  325  con1bii  346  con2bii  347  nbn  362  xor3  372  pm5.41  379  pm4.64  387  pm4.63  437  pm4.61  442  anor  510  pm4.53  513  pm4.55  515  pm4.56  516  pm4.57  518  pm4.25  537  pm4.87  607  anidm  675  pm4.77  827  anabs1  849  anabs7  851  an43  866  pm4.76  909  pm5.63  958  3ianor  1053  3oran  1055  pm3.2an3OLD  1239  syl3anbr  1367  3an6  1406  nannot  1450  nanbi  1451  truan  1498  truimfal  1512  nottru  1515  falbitru  1518  nic-dfim  1591  nic-dfneg  1592  2nalexn  1752  2nexaln  1754  sbequ8  1882  cleljust  1995  cleljustALT  2184  cleljustALT2  2185  dvelimf  2333  sb5rf  2421  sb6rf  2422  sb10f  2455  abeq1i  2733  nne  2794  necon3bbii  2837  necon2abii  2840  necon2bbii  2841  nnel  2902  rspc2gv  3310  ceqsrexbv  3325  clel2  3327  clel4  3330  2reu5lem1  3400  2reu5lem2  3401  2reu5lem3  3402  dfsbcq2  3425  cbvreucsf  3553  nss  3648  difab  3878  un0  3945  in0  3946  ss0b  3951  rexdifpr  4183  ssunsn2  4334  iindif2  4562  nssss  4895  epse  5067  restidsingOLD  5428  cotrg  5476  issref  5478  mptpreima  5597  ralrnmpt  6334  fmptsng  6399  fmptsnd  6400  dff14a  6492  f13dfv  6495  weniso  6569  uniuni  6935  suppvalbr  7259  eroveu  7802  isfinite2  8178  marypha1lem  8299  marypha2lem4  8304  infcllem  8353  wemapso2lem  8417  en3lplem2  8472  cantnfp1  8538  carden2  8773  fseqenlem1  8807  iscard3  8876  cardnum  8877  alephinit  8878  cardinfima  8880  alephiso  8881  dfac10b  8921  dfackm  8948  isfin5-2  9173  brdom7disj  9313  brdom6disj  9314  fsuppmapnn0fiubex  12748  hash2prb  13208  hashle2prv  13214  hashtpg  13221  wrd2ind  13431  splfv1  13459  cshwsexa  13523  s4f1o  13615  cotr2g  13665  relexpindlem  13753  lcmfunsnlem2  15296  ncoprmlnprm  15379  vdwapun  15621  cshwsiun  15749  cshwshash  15754  grpss  17380  pmtrfrn  17818  pmtrrn2  17820  pmtrprfvalrn  17848  issrg  18447  drngnidl  19169  drnglpir  19193  0ringnnzr  19209  unocv  19964  dsmmacl  20025  pmatcollpw2lem  20522  fvmptnn04if  20594  toptopon  20662  toprntopon  20669  ordtbas2  20935  ordtrest2  20948  xmeterval  22177  isclmp  22837  ovolfcl  23175  eldv  23602  eltayl  24052  musumsum  24852  umgrislfupgrlem  25946  ausgrusgrb  25987  cplgr3v  26252  vtxd0nedgb  26304  isrgr  26359  rgrusgrprc  26389  rgrprcx  26392  upgr2wlk  26467  pthsfval  26520  wlksnwwlknvbij  26706  usgr2wspthon  26760  isclwwlks  26781  clwwlksvbij  26822  iseupthf1o  26962  frcond2  27031  nfrgr2v  27034  4cycl2vnunb  27052  fusgr2wsp2nb  27090  frgrregord013  27141  lejdii  28285  mdslle1i  29064  mdslle2i  29065  mdslj1i  29066  mdslj2i  29067  mo5f  29213  unipreima  29329  2ndpreima  29369  ordtrest2NEW  29793  ordtconnlem1  29794  ballotlem2  30373  plymulx0  30446  bnj115  30552  bnj156  30557  bnj206  30560  bnj110  30689  bnj121  30701  bnj124  30702  bnj130  30705  bnj153  30711  bnj207  30712  bnj581  30739  bnj611  30749  bnj864  30753  bnj865  30754  bnj893  30759  bnj1000  30772  bnj978  30780  bnj1040  30801  bnj1049  30803  bnj1133  30818  bnj1189  30838  cnvco1  31411  cnvco2  31412  dfiota3  31725  trer  32005  nabi1i  32086  nabi2i  32087  bj-dfifc2  32259  bj-df-ifc  32260  bj-dfssb2  32335  bj-hbext  32396  bj-dvelimdv  32532  bj-cleljustab  32545  bj-denotes  32558  bj-ralcom4  32568  bj-rexcom4  32569  bj-elsngl  32656  bj-nuliotaALT  32720  bj-rest10  32731  bj-restuni  32740  con1bii2  32850  con2bii2  32851  topdifinfeq  32869  isbasisrelowllem2  32875  wl-sb8eut  33030  wl-clelv2-just  33050  inixp  33194  notbinot1  33549  notbinot2  33553  truconj  33574  sbccom2lem  33600  sbccom2  33601  sbccom2f  33602  tsim1  33608  tsxo3  33617  tsxo4  33618  isopos  33986  islvol5  34384  elpadd0  34614  dvhopellsm  35925  diblsmopel  35979  mapdvalc  36437  rmxypairf1o  36995  acsfn1p  37289  ifpnotnotb  37344  ifpdfxor  37352  ifpidg  37356  ifpim123g  37365  ifpim1g  37366  ifpimimb  37369  ifpimim  37374  rp-fakeanorass  37378  rp-isfinite6  37384  elmapintrab  37402  undmrnresiss  37430  clcnvlem  37450  cnviun  37462  dfxor4  37578  dfhe3  37590  dffrege69  37747  dffrege76  37754  or3or  37840  uneqsn  37842  pm10.252  38081  pm10.253  38082  pm10.42  38084  aaanv  38109  pm13.195  38135  pm13.196a  38136  sbc3or  38259  sbc3orgOLD  38263  en3lpVD  38602  3orbi123VD  38607  sbc3orgVD  38608  undif3VD  38640  ax6e2ndeqVD  38667  ax6e2ndeqALT  38689  sineq0ALT  38695  uzwo4  38743  rnmptpr  38867  fompt  38888  mapsnend  38900  allbutfiinf  39146  limsupequzmptlem  39396  cncfshift  39422  dvnmul  39495  dvnprodlem2  39499  rrxsnicc  39857  salexct  39889  sge00  39930  sge0iunmpt  39972  meadjiun  40020  carageneld  40053  ovncvrrp  40115  ovolval4lem1  40200  vonioo  40233  vonicc  40236  nsssmfmbf  40324  smfmullem4  40338  aibandbiaiffaiffb  40395  plcofph  40445  pldofph  40446  plvcofph  40447  plvcofphax  40448  plvofpos  40449  aovov0bi  40610  spr0nelg  41044  sprvalpwn0  41051  copisnmnd  41127  pgrpgt2nabl  41465  lindslinindsimp2lem5  41569  islininds2  41591  ldepslinc  41616  ssdifsn  41752
 Copyright terms: Public domain W3C validator