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

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

Proof of Theorem biimprcd
StepHypRef Expression
1 id 22 . 2
2 biimpcd.1 . 2
31, 2syl5ibrcom 222 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 184
This theorem is referenced by:  biimparc  487  ax12i  1738  axc9lem1  2001  axc9lem2  2040  ax12eq  2271  ax12el  2272  moanim  2350  euan  2351  eleq1a  2540  ceqsalgALT  3135  cgsexg  3142  cgsex2g  3143  cgsex4g  3144  ceqsex  3145  spc2egv  3196  spc3egv  3198  csbiebt  3454  dfiin2g  4363  ralxfrALT  4671  ordun  4984  opelxp  5034  ssrel  5096  ssrel2  5098  ssrelrel  5108  iss  5326  riotaclb  6295  iunpw  6614  limom  6715  funcnvuni  6753  fun11iun  6760  soxp  6913  tfrlem8  7072  oaordex  7226  eroveu  7425  fundmen  7609  nneneq  7720  onfin2  7729  dif1enOLD  7772  dif1en  7773  unfilem1  7804  rankwflemb  8232  sornom  8678  isf32lem9  8762  axdc3lem2  8852  axdc4lem  8856  zorn2lem3  8899  zorn2lem7  8903  tskuni  9182  grur1a  9218  grothomex  9228  genpnnp  9404  ltaddpr  9433  reclem4pr  9449  supmullem1  10534  uzin  11142  elfzmlbp  11815  sqrlem6  13081  sqreulem  13192  isprm2lem  14224  lubun  15753  lspsneq  17768  fvmptnn04ifb  19352  fbasfip  20369  alexsubALTlem2  20548  ovolunlem1  21908  dchrisum0flb  23695  brbtwn2  24208  axcontlem8  24274  usgranloopv  24378  rusgrargra  24930  frgrancvvdeqlemC  25039  grpomndo  25348  mdbr3  27216  mdbr4  27217  atssma  27297  atcvatlem  27304  ssrelf  27466  nepss  29095  fprb  29203  frrlem4  29390  nodmon  29410  nodenselem4  29444  nocvxminlem  29450  nofulllem4  29465  nofulllem5  29466  hfun  29835  supadd  30042  indexdom  30225  fdc  30238  totbndss  30273  ceqsex3OLD  30601  pm13.14  31316  isassintop  32534  tratrb  33307  ax6e2ndeq  33332  3impexpbicomVD  33657  tratrbVD  33661  equncomVD  33668  trsbcVD  33677  sbcssgVD  33683  csbingVD  33684  onfrALTVD  33691  csbsngVD  33693  csbxpgVD  33694  csbresgVD  33695  csbrngVD  33696  csbima12gALTVD  33697  csbunigVD  33698  csbfv12gALTVD  33699  con5VD  33700  hbimpgVD  33704  hbexgVD  33706  ax6e2ndeqVD  33709  bj-ax12i  34226  lsatn0  34724  lsatcmp  34728  lsatcv0  34756  lfl1dim  34846  lfl1dim2N  34847  lkrss2N  34894  lub0N  34914  glb0N  34918  ispsubcl2N  35671  cdlemefrs29bpre0  36122  dihglblem2N  37021  dihglblem3N  37022  dochsnnz  37177  rp-isfinite4  37742
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