MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  biimpcd Unicode version

Theorem biimpcd 224
Description: Deduce a commuted implication from a logical equivalence. (Contributed by NM, 3-May-1994.) (Proof shortened by Wolf Lammen, 22-Sep-2013.)
Hypothesis
Ref Expression
biimpcd.1
Assertion
Ref Expression
biimpcd

Proof of Theorem biimpcd
StepHypRef Expression
1 id 22 . 2
2 biimpcd.1 . 2
31, 2syl5ibcom 220 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 184
This theorem is referenced by:  biimpac  486  axc16i  2064  nelneq  2574  nelneq2  2575  nelne1  2786  nelne2  2787  nssne1  3559  nssne2  3560  psssstr  3609  difsn  4164  iununi  4415  disjiun  4442  nbrne1  4469  nbrne2  4470  mosubopt  4750  tz7.7  4909  issref  5385  tz6.12i  5891  ssimaex  5938  chfnrn  5998  fvn0ssdmfun  6022  ffnfv  6057  f1elima  6171  elovmpt3rab1  6536  limsssuc  6685  nnsuc  6717  peano5  6723  dftpos4  6993  odi  7247  fineqvlem  7754  pssnn  7758  ordunifi  7790  wdom2d  8027  r1pwss  8223  alephval3  8512  infdif  8610  cff1  8659  cofsmo  8670  axdc3lem2  8852  zorn2lem6  8902  cfpwsdom  8980  prub  9393  prnmadd  9396  1re  9616  letr  9699  dedekindle  9766  addid1  9781  xrletr  11390  0fz1  11734  elfzmlbp  11815  leisorel  12509  exprelprel  12528  brfi1uzind  12532  swrdccatfn  12707  sqrmo  13085  dvdseq  14033  isprm2  14225  nprmdvds1  14252  catsubcat  15208  pltletr  15601  mgm2nsgrplem3  16038  sgrp2nmndlem3  16043  fvcosymgeq  16454  sylow2alem2  16638  islss  17581  assamulgscmlem2  17998  gsumply1subr  18275  gzrngunitlem  18482  pjdm2  18742  dmatmul  18999  decpmatmullem  19272  monmat2matmon  19325  chpscmat  19343  chfacfscmulgsum  19361  chfacfpmmulgsum  19365  isclo2  19589  fbasfip  20369  ufileu  20420  alexsubALTlem2  20548  cnextcn  20567  metustblOLD  21083  metustbl  21084  usgrarnedg1  24389  nbgraf1olem3  24443  nbgraf1olem5  24445  nb3graprlem1  24451  cusgrafilem2  24480  wlkn0  24527  fargshiftfo  24638  3v3e3cycl1  24644  4cycl4v4e  24666  4cycl4dv4e  24668  wlkiswwlk2lem3  24693  wlklniswwlkn1  24699  wlklniswwlkn2  24700  wwlknext  24724  clwwlknimp  24776  clwlkisclwwlklem2a1  24779  clwlkisclwwlklem2a  24785  clwwlkel  24793  clwwlkext2edg  24802  wwlkext2clwwlk  24803  clwwisshclwwlem  24806  hashecclwwlkn1  24834  usghashecclwwlk  24835  clwlkfclwwlk  24844  clwlkf1clwwlklem2  24847  el2wlkonot  24869  el2wlkonotot1  24874  frgrancvvdeqlemA  25037  frgrancvvdeqlemC  25039  frgraeu  25054  numclwlk2lem2f  25103  numclwlk2lem2f1o  25105  frgraogt3nreg  25120  ismgmOLD  25322  5oalem6  26577  eigorthi  26756  adjbd1o  27004  dmdbr7ati  27343  dfpo2  29184  fundmpss  29196  funbreq  29201  idinside  29734  sdclem2  30235  fdc1  30239  lptioo2  31637  lptioo1  31638  funressnfv  32213  ffnafv  32256  usgedgimp  32403  usgedgimpALT  32406  fusgraimpcl  32427  fusgraimpclALT  32429  fusgraimpclALT2  32431  mgmpropd  32463  funcestrcsetclem8  32653  funcestrcsetclem9  32654  fthestrcsetc  32656  fullestrcsetc  32657  funcsetcestrclem9  32669  fthsetcestrc  32671  fullsetcestrc  32672  rngcinv  32789  rngcinvOLD  32801  ringcinv  32840  ringcinvOLD  32864  srhmsubc  32884  srhmsubcOLD  32903  3impexpbicom  33221  sbcim2g  33309  suctrALT2VD  33636  suctrALT2  33637  3impexpVD  33656  3impexpbicomVD  33657  sbcim2gVD  33675  csbeq2gVD  33692  csbsngVD  33693  ax6e2ndeqVD  33709  2sb5ndVD  33710  bj-eldiag2  34607  lsatcvatlem  34774  atnle  35042  cvratlem  35145  ispsubcl2N  35671  trlord  36295  diaelrnN  36772  cdlemm10N  36845  dochexmidlem7  37193
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 185
  Copyright terms: Public domain W3C validator