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  2024  nelneq  2571  nelneq2  2572  nelne1  2782  nelne2  2783  nssne1  3526  nssne2  3527  psssstr  3576  difsn  4125  iununi  4372  disjiun  4399  nbrne1  4426  nbrne2  4427  mosubopt  4706  tz7.7  4862  issref  5330  tz6.12i  5833  ssimaex  5879  chfnrn  5937  ffnfv  5992  f1elima  6101  limsssuc  6594  nnsuc  6626  peano5  6632  dftpos4  6898  odi  7152  fineqvlem  7662  pssnn  7666  ordunifi  7697  wdom2d  7932  r1pwss  8128  alephval3  8417  infdif  8515  cff1  8564  cofsmo  8575  axdc3lem2  8757  zorn2lem6  8807  cfpwsdom  8885  prub  9300  prnmadd  9303  1re  9522  letr  9605  dedekindle  9671  addid1  9686  xrletr  11271  0fz1  11614  elfzmlbp  11636  leisorel  12371  brfi1uzind  12377  swrdccatfn  12531  sqrmo  12899  dvdseq  13738  isprm2  13929  nprmdvds1  13955  pltletr  15300  fvcosymgeq  16093  sylow2alem2  16278  islss  17192  gsumply1subr  17869  gzrngunitlem  18070  pjdm2  18329  dmatmul  18587  decpmatmullem  18843  monmat2matmon  18895  isclo2  19091  fbasfip  19840  ufileu  19891  alexsubALTlem2  20019  cnextcn  20038  metustblOLD  20554  metustbl  20555  usgrarnedg1  23776  nbgraf1olem3  23821  nbgraf1olem5  23823  nb3graprlem1  23828  cusgrafilem2  23857  fargshiftfo  23993  3v3e3cycl1  23999  4cycl4v4e  24021  4cycl4dv4e  24023  ismgm  24276  5oalem6  25531  eigorthi  25710  adjbd1o  25958  dmdbr7ati  26297  dfpo2  28021  fundmpss  28033  funbreq  28038  idinside  28571  sdclem2  29098  fdc1  29102  funressnfv  30911  ffnafv  30954  elovmpt3rab1  31040  exprelprel  31106  wlkn0  31156  wlkiswwlk2lem3  31204  wlklniswwlkn1  31210  wlklniswwlkn2  31211  wwlknext  31233  el2wlkonot  31265  el2wlkonotot1  31270  clwwlknimp  31316  clwlkisclwwlklem2a1  31318  clwlkisclwwlklem2a  31324  clwwlkel  31332  clwwlkext2edg  31341  wwlkext2clwwlk  31342  clwwisshclwwlem  31347  hashecclwwlkn1  31385  usghashecclwwlk  31386  clwlkfclwwlk  31394  clwlkf1clwwlklem2  31397  frgrancvvdeqlemA  31507  frgrancvvdeqlemC  31509  frgraeu  31524  numclwlk2lem2f  31573  numclwlk2lem2f1o  31575  frgraogt3nreg  31590  assamulgscmlem2  31680  chpscmat  31840  chfacfscmulgsum  31858  chfacfpmmulgsum  31862  3impexpbicom  31999  sbcim2g  32088  suctrALT2VD  32415  suctrALT2  32416  3impexpVD  32435  3impexpbicomVD  32436  sbcim2gVD  32454  csbeq2gVD  32471  csbsngVD  32472  ax6e2ndeqVD  32488  2sb5ndVD  32489  lsatcvatlem  33545  atnle  33813  cvratlem  33916  ispsubcl2N  34442  trlord  35064  diaelrnN  35541  cdlemm10N  35614  dochexmidlem7  35962
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