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.64  386  pm4.63  436  pm4.61  441  anor  509  pm4.53  512  pm4.55  514  pm4.56  515  pm4.57  517  pm4.25  536  pm4.87  607  anidm  677  pm4.77  845  anabs1  867  anabs7  869  an43  884  pm4.76  928  pm5.63  979  3anor  1075  3ianorOLD  1076  3oran  1077  syl3anbr  1410  3an6  1449  nannot  1493  nanbi  1494  truan  1541  truimfal  1555  nottru  1558  falbitru  1561  nic-dfim  1634  nic-dfneg  1635  2nalexn  1795  2nexaln  1797  sbequ8  1942  cleljust  2038  cleljustALT  2221  cleljustALT2  2222  dvelimf  2365  sb5rf  2450  sb6rf  2451  sb10f  2484  abeq1i  2765  nne  2827  necon3bbii  2870  necon2abii  2873  necon2bbii  2874  nnel  2935  rspc2gv  3352  ceqsrexbv  3368  clel4  3374  rabeqc  3394  2reu5lem1  3446  2reu5lem2  3447  2reu5lem3  3448  dfsbcq2  3471  cbvreucsf  3600  nss  3696  difab  3929  un0  4000  in0  4001  ss0b  4006  rexdifpr  4238  ssdifsn  4351  ssunsn2  4391  iindif2  4621  nssss  4954  epse  5126  restidsingOLD  5494  cotrg  5542  issref  5544  mptpreima  5666  ralrnmpt  6408  fmptsng  6475  fmptsnd  6476  dff14a  6567  f13dfv  6570  weniso  6644  abnex  7007  uniuni  7013  suppvalbr  7344  eroveu  7885  isfinite2  8259  marypha1lem  8380  marypha2lem4  8385  infcllem  8434  wemapso2lem  8498  en3lplem2  8550  cantnfp1  8616  carden2  8851  fseqenlem1  8885  iscard3  8954  cardnum  8955  alephinit  8956  cardinfima  8958  alephiso  8959  dfac10b  8999  dfackm  9026  isfin5-2  9251  brdom7disj  9391  brdom6disj  9392  fsuppmapnn0fiubex  12832  hash2prb  13292  hashle2prv  13298  hashtpg  13305  wrd2ind  13523  splfv1  13552  cshwsexa  13616  s4f1o  13709  cotr2g  13761  relexpindlem  13847  lcmfunsnlem2  15400  ncoprmlnprm  15483  vdwapun  15725  cshwsiun  15853  cshwshash  15858  grpss  17487  pmtrfrn  17924  pmtrrn2  17926  pmtrprfvalrn  17954  issrg  18553  drngnidl  19277  drnglpir  19301  0ringnnzr  19317  unocv  20072  dsmmacl  20133  pmatcollpw2lem  20630  fvmptnn04if  20702  toptopon  20770  toprntopon  20777  ordtbas2  21043  ordtrest2  21056  xmeterval  22284  isclmp  22943  ovolfcl  23281  eldv  23707  eltayl  24159  musumsum  24963  umgrislfupgrlem  26062  numedglnl  26084  ausgrusgrb  26105  cplgr3v  26387  vtxd0nedgb  26440  finsumvtxdg2ssteplem1  26497  isrgr  26511  rgrusgrprc  26541  rgrprcx  26544  upgr2wlk  26620  pthsfval  26673  wlksnwwlknvbij  26871  wwlksnwwlksnon  26878  usgr2wspthon  26932  isclwwlk  26952  clwwlkvbij  27088  clwwlkvbijOLD  27089  iseupthf1o  27180  frcond2  27247  nfrgr2v  27252  4cycl2vnunb  27270  fusgr2wsp2nb  27314  frgrregord013  27382  lejdii  28525  mdslle1i  29304  mdslle2i  29305  mdslj1i  29306  mdslj2i  29307  mo5f  29452  unipreima  29574  2ndpreima  29613  ordtrest2NEW  30097  ordtconnlem1  30098  ballotlem2  30678  plymulx0  30752  bnj115  30919  bnj156  30922  bnj206  30925  bnj110  31054  bnj121  31066  bnj124  31067  bnj130  31070  bnj153  31076  bnj207  31077  bnj581  31104  bnj611  31114  bnj864  31118  bnj865  31119  bnj893  31124  bnj1000  31137  bnj978  31145  bnj1040  31166  bnj1049  31168  bnj1133  31183  bnj1189  31203  cnvco1  31775  cnvco2  31776  dfiota3  32155  trer  32435  nabi1i  32516  nabi2i  32517  bj-dfifc2  32689  bj-df-ifc  32690  bj-dfssb2  32765  bj-hbext  32826  bj-dvelimdv  32959  bj-cleljustab  32972  bj-denotes  32983  bj-ralcom4  32993  bj-rexcom4  32994  bj-elsngl  33081  bj-nuliotaALT  33145  bj-rest10  33166  bj-restuni  33175  bj-ismooredr2  33190  con1bii2  33309  con2bii2  33310  topdifinfeq  33328  isbasisrelowllem2  33334  wl-sb8eut  33489  wl-clelv2-just  33509  inixp  33653  notbinot1  34008  notbinot2  34012  truconj  34033  sbccom2lem  34059  sbccom2  34060  sbccom2f  34061  tsim1  34067  tsxo3  34076  tsxo4  34077  trcoss2  34374  isopos  34785  islvol5  35183  elpadd0  35413  dvhopellsm  36723  diblsmopel  36777  mapdvalc  37235  rmxypairf1o  37793  acsfn1p  38086  ifpnotnotb  38141  ifpdfxor  38149  ifpidg  38153  ifpim123g  38162  ifpim1g  38163  ifpimimb  38166  ifpimim  38171  rp-fakeanorass  38175  rp-isfinite6  38181  elmapintrab  38199  undmrnresiss  38227  clcnvlem  38247  cnviun  38259  dfxor4  38375  dfhe3  38386  dffrege69  38543  dffrege76  38550  or3or  38636  uneqsn  38638  pm10.252  38877  pm10.253  38878  pm10.42  38880  aaanv  38905  pm13.195  38931  pm13.196a  38932  sbc3or  39055  sbc3orgOLD  39059  en3lpVD  39394  3orbi123VD  39399  sbc3orgVD  39400  undif3VD  39432  ax6e2ndeqVD  39459  ax6e2ndeqALT  39481  sineq0ALT  39487  uzwo4  39535  rnmptpr  39672  fompt  39693  mapsnend  39705  allbutfiinf  39960  limsupequzmptlem  40278  cncfshift  40405  dvnmul  40476  dvnprodlem2  40480  rrxsnicc  40838  salexct  40870  sge00  40911  sge0iunmpt  40953  meadjiun  41001  carageneld  41037  ovncvrrp  41099  ovolval4lem1  41184  vonioo  41217  vonicc  41220  nsssmfmbf  41308  smfmullem4  41322  aibandbiaiffaiffb  41382  plcofph  41432  pldofph  41433  plvcofph  41434  plvcofphax  41435  plvofpos  41436  aovov0bi  41597  4an21  41611  spr0nelg  42051  sprvalpwn0  42058  copisnmnd  42134  pgrpgt2nabl  42472  lindslinindsimp2lem5  42576  islininds2  42598  ldepslinc  42623
 Copyright terms: Public domain W3C validator