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  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  1887  cleljust  2000  cleljustALT  2189  cleljustALT2  2190  dvelimf  2338  sb5rf  2426  sb6rf  2427  sb10f  2460  abeq1i  2739  nne  2800  necon3bbii  2843  necon2abii  2846  necon2bbii  2847  nnel  2908  ceqsrexbv  3325  clel2  3327  clel4  3330  2reu5lem1  3400  2reu5lem2  3401  2reu5lem3  3402  dfsbcq2  3425  cbvreucsf  3553  nss  3647  difab  3877  un0  3944  in0  3945  ss0b  3950  rexdifpr  4181  ssunsn2  4332  iindif2  4560  nssss  4890  epse  5062  restidsingOLD  5422  cotrg  5470  issref  5472  mptpreima  5590  ralrnmpt  6325  fmptsng  6389  fmptsnd  6390  dff14a  6482  f13dfv  6485  weniso  6559  uniuni  6921  suppvalbr  7245  eroveu  7788  isfinite2  8163  marypha1lem  8284  marypha2lem4  8289  infcllem  8338  wemapso2lem  8402  en3lplem2  8457  cantnfp1  8523  carden2  8758  fseqenlem1  8792  iscard3  8861  cardnum  8862  alephinit  8863  cardinfima  8865  alephiso  8866  dfac10b  8906  dfackm  8933  isfin5-2  9158  brdom7disj  9298  brdom6disj  9299  fsuppmapnn0fiubex  12729  hash2prb  13189  hashtpg  13200  wrd2ind  13410  splfv1  13438  cshwsexa  13502  s4f1o  13594  cotr2g  13644  relexpindlem  13732  lcmfunsnlem2  15272  ncoprmlnprm  15355  vdwapun  15597  cshwsiun  15725  cshwshash  15730  grpss  17356  pmtrfrn  17794  pmtrrn2  17796  pmtrprfvalrn  17824  issrg  18423  drngnidl  19143  drnglpir  19167  0ringnnzr  19183  unocv  19938  dsmmacl  19999  pmatcollpw2lem  20496  fvmptnn04if  20568  toptopon  20643  ordtbas2  20900  ordtrest2  20913  xmeterval  22142  isclmp  22800  ovolfcl  23137  eldv  23563  eltayl  24013  musumsum  24813  umgrislfupgrlem  25907  ausgrusgrb  25947  cplgr3v  26212  vtxd0nedgb  26264  isrgr  26319  rgrusgrprc  26349  rgrprcx  26352  upgr2wlk  26427  pthsfval  26480  wlksnwwlknvbij  26666  usgr2wspthon  26720  isclwwlks  26741  clwwlksvbij  26782  iseupthf1o  26922  frcond2  26991  nfrgr2v  26994  4cycl2vnunb  27012  fusgr2wsp2nb  27050  frgrregord013  27101  lejdii  28237  mdslle1i  29016  mdslle2i  29017  mdslj1i  29018  mdslj2i  29019  mo5f  29164  unipreima  29279  2ndpreima  29319  ordtrest2NEW  29743  ordtconnlem1  29744  ballotlem2  30323  plymulx0  30396  bnj115  30491  bnj156  30496  bnj206  30499  bnj110  30628  bnj121  30640  bnj124  30641  bnj130  30644  bnj153  30650  bnj207  30651  bnj581  30678  bnj611  30688  bnj864  30692  bnj865  30693  bnj893  30698  bnj1000  30711  bnj978  30719  bnj1040  30740  bnj1049  30742  bnj1133  30757  bnj1189  30777  cnvco1  31349  cnvco2  31350  dfiota3  31645  trer  31925  nabi1i  32006  nabi2i  32007  bj-dfifc2  32179  bj-df-ifc  32180  bj-dfssb2  32255  bj-hbext  32316  bj-dvelimdv  32452  bj-cleljustab  32465  bj-denotes  32478  bj-ralcom4  32488  bj-rexcom4  32489  bj-elsngl  32576  bj-nuliotaALT  32640  bj-rest10  32651  bj-restuni  32660  bj-sspwpw  32667  bj-toprntopon  32673  con1bii2  32784  con2bii2  32785  topdifinfeq  32803  isbasisrelowllem2  32809  wl-sb8eut  32967  inixp  33122  notbinot1  33477  notbinot2  33481  truconj  33502  sbccom2lem  33528  sbccom2  33529  sbccom2f  33530  tsim1  33536  tsxo3  33545  tsxo4  33546  isopos  33914  islvol5  34312  elpadd0  34542  dvhopellsm  35853  diblsmopel  35907  mapdvalc  36365  rmxypairf1o  36923  acsfn1p  37217  ifpnotnotb  37272  ifpdfxor  37280  ifpidg  37284  ifpim123g  37293  ifpim1g  37294  ifpimimb  37297  ifpimim  37302  rp-fakeanorass  37306  rp-isfinite6  37312  elmapintrab  37330  undmrnresiss  37358  clcnvlem  37378  cnviun  37390  dfxor4  37506  dfhe3  37518  dffrege69  37675  dffrege76  37682  or3or  37768  uneqsn  37770  pm10.252  38009  pm10.253  38010  pm10.42  38012  aaanv  38037  pm13.195  38063  pm13.196a  38064  sbc3or  38187  sbc3orgOLD  38191  en3lpVD  38530  3orbi123VD  38535  sbc3orgVD  38536  undif3VD  38568  ax6e2ndeqVD  38595  ax6e2ndeqALT  38617  sineq0ALT  38623  uzwo4  38673  rnmptpr  38799  fompt  38820  mapsnend  38832  allbutfiinf  39079  limsupequzmptlem  39332  cncfshift  39358  dvnmul  39432  dvnprodlem2  39436  rrxsnicc  39795  salexct  39827  sge00  39868  sge0iunmpt  39910  meadjiun  39958  carageneld  39991  ovncvrrp  40053  ovolval4lem1  40138  vonioo  40171  vonicc  40174  nsssmfmbf  40262  smfmullem4  40276  aibandbiaiffaiffb  40333  plcofph  40383  pldofph  40384  plvcofph  40385  plvcofphax  40386  plvofpos  40387  aovov0bi  40548  spr0nelg  40983  sprvalpwn0  40990  copisnmnd  41051  pgrpgt2nabl  41390  lindslinindsimp2lem5  41494  islininds2  41516  ldepslinc  41541  ssdifsn  41677
  Copyright terms: Public domain W3C validator