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

Theorem biimpcd 239
 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 235 1 (𝜓 → (𝜑𝜒))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ 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:  biimpac  504  axc16i  2460  nelneq  2861  nelneq2  2862  nelne1  3026  nelne2  3027  nssne1  3800  nssne2  3801  psssstr  3853  prproe  4584  iununi  4760  disjiun  4790  nbrne1  4821  nbrne2  4822  propeqop  5116  mosubopt  5118  issref  5665  tz7.7  5908  suctr  5967  tz6.12i  6373  ssimaex  6423  chfnrn  6489  fvn0ssdmfun  6511  ffnfv  6549  f1elima  6681  elovmpt3rab1  7056  limsssuc  7213  nnsuc  7245  peano5  7252  dftpos4  7538  odi  7826  fineqvlem  8337  pssnn  8341  ordunifi  8373  wdom2d  8648  r1pwss  8818  alephval3  9121  infdif  9221  cff1  9270  cofsmo  9281  axdc3lem2  9463  zorn2lem6  9513  cfpwsdom  9596  prub  10006  prnmadd  10009  1re  10229  letr  10321  dedekindle  10391  addid1  10406  negf1o  10650  negfi  11161  xrletr  12180  0fz1  12552  elfzmlbp  12642  leisorel  13434  elss2prb  13459  exprelprel  13461  fi1uzind  13469  swrdnd  13630  swrdccatfn  13680  sqrmo  14189  isprm2  15595  nprmdvds1  15618  oddprmdvds  15807  catsubcat  16698  funcestrcsetclem8  16986  funcestrcsetclem9  16987  fthestrcsetc  16989  fullestrcsetc  16990  funcsetcestrclem9  17002  fthsetcestrc  17004  fullsetcestrc  17005  pltletr  17170  issstrmgm  17451  mgm2nsgrplem3  17606  sgrp2nmndlem3  17611  fvcosymgeq  18047  sylow2alem2  18231  islss  19135  assamulgscmlem2  19549  gsumply1subr  19804  gzrngunitlem  20011  pjdm2  20255  dmatmul  20503  decpmatmullem  20776  monmat2matmon  20829  chpscmat  20847  chfacfscmulgsum  20865  chfacfpmmulgsum  20869  isclo2  21092  fbasfip  21871  ufileu  21922  alexsubALTlem2  22051  cnextcn  22070  metustbl  22570  ushgredgedg  26318  ushgredgedgloop  26320  edgnbusgreu  26465  nb3grprlem1  26478  cusgrfilem1  26559  cusgrfilem2  26560  umgr2v2evtxel  26626  wlkcompim  26735  usgr2pth  26868  usgr2trlncrct  26907  wwlknp  26944  wlkiswwlks2lem3  26978  wlkiswwlksupgr2  26984  wlklnwwlkln2lem  26989  wwlksnext  27009  2pthdlem1  27048  umgr2adedgwlkonALT  27065  umgr2wlkon  27068  elwspths2spth  27087  rusgr0edg  27093  clwlkclwwlklem2a1  27113  clwlkclwwlklem2a  27119  clwwisshclwwslem  27135  loopclwwlkn1b  27169  clwwlkel  27173  clwwlkext2edg  27184  wwlksext2clwwlk  27185  wwlksext2clwwlkOLD  27186  hashecclwwlkn1  27206  umgrhashecclwwlk  27207  clwlksfclwwlkOLD  27214  clwlksf1clwwlklem2OLD  27218  uhgr3cyclexlem  27331  upgr4cycl4dv4e  27335  eupth2lem3lem4  27381  frgruhgr0v  27415  numclwlk1lem2f1  27514  numclwlk2lem2f  27536  numclwlk2lem2f1o  27538  numclwlk2lem2fOLD  27543  numclwlk2lem2f1oOLD  27545  frgrogt3nreg  27563  5oalem6  28825  eigorthi  29003  adjbd1o  29251  dmdbr7ati  29590  dfpo2  31950  fundmpss  31969  funbreq  31973  idinside  32495  bj-eldiag2  33401  poimirlem32  33752  sdclem2  33849  fdc1  33853  ismgmOLD  33960  lsatcvatlem  34837  atnle  35105  cvratlem  35208  ispsubcl2N  35734  trlord  36357  diaelrnN  36834  cdlemm10N  36907  dochexmidlem7  37255  3impexpbicom  39185  sbcim2g  39248  suctrALT2VD  39568  suctrALT2  39569  3impexpVD  39588  3impexpbicomVD  39589  sbcim2gVD  39608  csbeq2gVD  39625  csbsngVD  39626  ax6e2ndeqVD  39642  2sb5ndVD  39643  infxrunb3rnmpt  40151  lptioo2  40364  lptioo1  40365  funressnfv  41712  ffnafv  41755  iccpartiltu  41866  iccpartigtl  41867  icceuelpartlem  41879  fargshiftfo  41886  bgoldbtbndlem2  42202  mgmpropd  42283  rngcinv  42489  rngcinvALTV  42501  ringcinv  42540  ringcinvALTV  42564  srhmsubc  42584  srhmsubcALTV  42602  nnolog2flm1  42892
 Copyright terms: Public domain W3C validator