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  1744  2nexaln  1746  sbequ8  1871  cleljust  1984  cleljustALT  2172  cleljustALT2  2173  dvelimf  2321  sb5rf  2409  sb6rf  2410  sb10f  2443  abeq1i  2722  nne  2785  necon3bbii  2828  necon2abii  2831  necon2bbii  2832  nnel  2891  ceqsrexbv  3306  clel2  3308  clel4  3311  2reu5lem1  3379  2reu5lem2  3380  2reu5lem3  3381  dfsbcq2  3404  cbvreucsf  3532  nss  3625  difab  3854  un0  3918  in0  3919  ss0b  3924  ssunsn2  4296  iindif2  4519  nssss  4845  epse  5011  restidsingOLD  5365  cotrg  5413  issref  5415  mptpreima  5531  ralrnmpt  6261  fmptsng  6317  fmptsnd  6318  dff14a  6405  f13dfv  6408  weniso  6482  fvmptopab2  6573  uniuni  6842  suppvalbr  7163  eroveu  7706  isfinite2  8080  marypha1lem  8199  marypha2lem4  8204  infcllem  8253  wemapso2lem  8317  en3lplem2  8372  cantnfp1  8438  carden2  8673  fseqenlem1  8707  iscard3  8776  cardnum  8777  alephinit  8778  cardinfima  8780  alephiso  8781  dfac10b  8821  dfackm  8848  isfin5-2  9073  brdom7disj  9211  brdom6disj  9212  fsuppmapnn0fiubex  12609  hash2prb  13063  hashtpg  13071  wrd2ind  13275  splfv1  13303  cshwsexa  13367  s4f1o  13459  cotr2g  13509  relexpindlem  13597  lcmfunsnlem2  15137  ncoprmlnprm  15220  vdwapun  15462  cshwsiun  15590  cshwshash  15595  grpss  17209  pmtrfrn  17647  pmtrrn2  17649  pmtrprfvalrn  17677  issrg  18276  drngnidl  18996  drnglpir  19020  0ringnnzr  19036  unocv  19785  dsmmacl  19846  pmatcollpw2lem  20343  fvmptnn04if  20415  toptopon  20490  ordtbas2  20747  ordtrest2  20760  xmeterval  21988  isclmp  22636  ovolfcl  22959  eldv  23385  eltayl  23835  musumsum  24635  usgrafilem1  25706  trls  25832  is2wlk  25861  wwlknndef  26031  wlknwwlknvbij  26034  clwwlknndef  26067  clwwlkvbij  26095  el2wlkonotot0  26165  usg2spthonot0  26182  frgraun  26289  frgra2v  26292  4cycl2vnunb  26310  vdn0frgrav2  26316  vdgn0frgrav2  26317  2spotdisj  26354  usg2spot2nb  26358  usgreg2spot  26360  frgraregord013  26411  lejdii  27587  mdslle1i  28366  mdslle2i  28367  mdslj1i  28368  mdslj2i  28369  mo5f  28514  unipreima  28632  2ndpreima  28674  ordtrest2NEW  29103  ordtconlem1  29104  ballotlem2  29683  plymulx0  29756  bnj115  29851  bnj156  29856  bnj206  29859  bnj110  29988  bnj121  30000  bnj124  30001  bnj130  30004  bnj153  30010  bnj207  30011  bnj581  30038  bnj611  30048  bnj864  30052  bnj865  30053  bnj893  30058  bnj1000  30071  bnj978  30079  bnj1040  30100  bnj1049  30102  bnj1133  30117  bnj1189  30137  cnvco1  30709  cnvco2  30710  dfiota3  31006  trer  31286  nabi1i  31367  nabi2i  31368  bj-dfifc2  31540  bj-df-ifc  31541  bj-nf3  31573  bj-dfssb2  31635  bj-hbext  31694  bj-denotes  31848  bj-ralcom4  31858  bj-rexcom4  31859  bj-elsngl  31945  bj-nuliotaALT  32007  bj-rest10  32018  bj-restuni  32027  bj-sspwpw  32034  bj-toprntopon  32040  con1bii2  32151  con2bii2  32152  topdifinfeq  32170  isbasisrelowllem2  32176  wl-sb8eut  32334  inixp  32489  notbinot1  32844  notbinot2  32848  truconj  32869  sbccom2lem  32895  sbccom2  32896  sbccom2f  32897  tsim1  32903  tsxo3  32912  tsxo4  32913  isopos  33281  islvol5  33679  elpadd0  33909  dvhopellsm  35220  diblsmopel  35274  mapdvalc  35732  rmxypairf1o  36290  acsfn1p  36584  ifpnotnotb  36639  ifpdfxor  36647  ifpidg  36651  ifpim123g  36660  ifpim1g  36661  ifpimimb  36664  ifpimim  36669  rp-fakeanorass  36673  rp-isfinite6  36679  elmapintrab  36697  undmrnresiss  36725  clcnvlem  36745  cnviun  36757  dfxor4  36873  dfhe3  36885  dffrege69  37042  dffrege76  37049  or3or  37135  uneqsn  37137  pm10.252  37378  pm10.253  37379  pm10.42  37381  aaanv  37406  pm13.195  37432  pm13.196a  37433  sbc3or  37555  sbc3orgOLD  37559  en3lpVD  37898  3orbi123VD  37903  sbc3orgVD  37904  undif3VD  37936  ax6e2ndeqVD  37963  ax6e2ndeqALT  37985  sineq0ALT  37991  uzwo4  38042  inn0f  38064  rnmptpr  38149  fompt  38170  mapsnend  38182  cncfshift  38556  dvnmul  38630  dvnprodlem2  38634  rrxsnicc  38993  salexct  39025  sge00  39066  sge0iunmpt  39108  meadjiun  39156  carageneld  39189  ovncvrrp  39251  ovolval4lem1  39336  vonioo  39370  vonicc  39373  nsssmfmbf  39462  smfmullem4  39476  aibandbiaiffaiffb  39507  plcofph  39557  pldofph  39558  plvcofph  39559  plvcofphax  39560  plvofpos  39561  aovov0bi  39723  rexdifpr  40114  umgrislfupgrlem  40342  ausgrusgrb  40390  cplgr3v  40652  vtxd0nedgb  40698  isrgr  40754  rgrusgrprc  40784  rgrprcx  40787  upgr2wlk  40871  wlksnwwlknvbij  41109  usgr2wspthon  41163  isclwwlks  41183  clwwlksvbij  41224  frcond2  41434  nfrgr2v  41437  4cycl2vnunb-av  41455  fusgr2wsp2nb  41493  av-frgraregord013  41544  copisnmnd  41594  pgrpgt2nabl  41936  lindslinindsimp2lem5  42040  islininds2  42062  ldepslinc  42087
  Copyright terms: Public domain W3C validator