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

Theorem biimprd 239
Description: Deduce a converse implication from a logical equivalence. Deduction associated with biimpr 211 and biimpri 219. (Contributed by NM, 11-Jan-1993.) (Proof shortened by Wolf Lammen, 22-Sep-2013.)
Hypothesis
Ref Expression
biimprd.1 (𝜑 → (𝜓𝜒))
Assertion
Ref Expression
biimprd (𝜑 → (𝜒𝜓))

Proof of Theorem biimprd
StepHypRef Expression
1 id 22 . 2 (𝜒𝜒)
2 biimprd.1 . 2 (𝜑 → (𝜓𝜒))
31, 2syl5ibr 237 1 (𝜑 → (𝜒𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197
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 198
This theorem is referenced by:  syl6bir  245  mpbird  248  sylibrd  250  sylbird  251  con4bid  308  mtbid  315  mtbii  317  imbi1d  332  biimpar  465  prlem1  1070  alexbii  1917  spfw  2133  spfwOLD  2134  cbvalw  2136  alcomiw  2139  alcomiwOLD  2140  cbvalv1  2350  nfimdOLD  2402  cbval  2446  axc16i  2486  axc16gALT  2528  eqrdav  2816  pm13.18  3070  rspcimdv  3514  rspcedv  3517  moi2  3596  moi  3598  eqrdOLD  3829  sspsstr  3921  rabsnifsb  4459  ralxfr2d  5092  isso2i  5277  wefrc  5318  elinxp  5651  elresOLD  5653  sotri3  5751  oneqmini  6002  ordsssuc2  6039  ordtri2or  6046  2elresin  6223  f1ocnv  6375  tz6.12c  6443  fveqres  6460  fvun1  6500  dffo4  6607  funopsn  6647  fconst5  6706  fnprb  6707  fntpb  6708  isores3  6819  f1owe  6837  weniso  6838  ndmovordi  7065  abnexg  7204  orduniorsuc  7270  ordzsl  7285  tfinds  7299  f1oweALT  7392  fnse  7538  tposfo2  7620  wfrlem5  7665  wfrlem12  7672  issmo2  7692  iordsmo  7700  smoel2  7706  tz7.48lem  7782  oawordeulem  7881  om00  7902  omlimcl  7905  odi  7906  nnawordi  7948  fiint  8486  fipreima  8521  dffi2  8578  suplub2  8616  wemapsolem  8704  unwdomg  8738  inf3lem3  8784  trcl  8861  fidomtri  9112  prdom2  9122  cardaleph  9205  ackbij1lem16  9352  coflim  9378  coftr  9390  infpssrlem4  9423  isfin7-2  9513  axdc3lem2  9568  axdc3lem4  9570  brdom6disj  9649  entric  9674  fpwwe2lem12  9758  inatsk  9895  grur1a  9936  indpi  10024  reclem3pr  10166  supsrlem  10227  lelttr  10423  dedekindle  10496  negn0  10754  fimaxre  11263  nnmulcl  11340  nnmulclOLD  11341  arch  11576  nnnegz  11666  zeo  11749  uzm1  11956  rpneg  12097  xrlttri  12208  xrlelttr  12225  iccid  12458  icoshft  12535  fzen  12601  elfz1b  12652  elfz2nn0  12674  elfzom1p1elfzo  12792  fleqceilz  12897  zmodidfzoimp  12944  modsumfzodifsn  12987  hasheqf1oi  13380  hashnfinnn0  13390  hashle2prv  13497  swrd0  13678  swrdccatin12lem2  13733  swrdccat  13737  swrdccat3blem  13739  repswswrd  13775  trclublem  13979  max0add  14293  abslt  14297  absle  14298  rexuzre  14335  caurcvg  14650  caucvg  14652  dvdsval2  15226  negdvdsb  15241  muldvds2  15250  dvdsabseq  15278  smuval2  15443  smupvallem  15444  rplpwr  15515  alginv  15527  algfx  15532  coprmgcdb  15601  divgcdcoprm0  15617  prmgt1  15647  oddprmgt2  15649  rpexp1i  15670  qnumdencl  15684  phiprmpw  15718  prmdiveq  15728  prm23lt5  15756  pcmpt  15833  infpnlem1  15851  prmgaplem3  15994  prmgaplem8  15999  imasaddfnlem  16413  plelttr  17197  lubval  17209  lublecllem  17213  glbval  17222  mrcmndind  17591  mndodconglem  18181  elfrlmbasn0  20337  mavmulsolcl  20589  slesolex  20721  fvmptnn04if  20888  chfacfisf  20893  chfacfisfcpmat  20894  cnpnei  21303  unconn  21467  comppfsc  21570  kqsat  21769  isr0  21775  qtophmeo  21855  trufil  21948  alexsubALT  22089  cnextcn  22105  ucnima  22319  iducn  22321  bl2in  22439  addcnlem  22901  rescncf  22934  ovoliunlem2  23507  voliun  23558  mbflimsup  23670  itgcn  23846  dvdsq1p  24157  aalioulem2  24325  recosf1o  24519  logrec  24738  xrlimcnp  24932  basellem4  25047  bposlem1  25246  bposlem5  25250  lgsqrmod  25314  lgsdchrval  25316  2lgslem1a1  25351  pntlem3  25535  brbtwn2  26022  axbtwnid  26056  umgredgprv  26239  umgrpredgv  26273  usgredgprvALT  26325  fusgrfisstep  26460  fusgrfis  26461  nbupgr  26479  nbumgrvtx  26481  finsumvtxdg2size  26697  wlkp1lem8  26828  upgr2pthnlp  26879  wwlksnextinj  27059  usgr2wspthons3  27129  clwlkclwwlklem2a1  27158  clwwisshclwws  27181  clwwlknonex2lem2  27300  eucrctshift  27439  eucrct2eupth  27441  numclwwlk2lem1  27579  numclwwlk2lem1OLD  27586  numclwwlk5lem  27598  frgrreggt1  27604  frgrreg  27605  friendship  27610  blocn2  28014  htthlem  28125  axhcompl-zf  28206  spanuni  28754  spansncol  28778  spansneleq  28780  elspansn5  28784  idcnop  29191  pjnormssi  29378  dmdmd  29510  bian1d  29657  ifeqeqx  29709  opabssi  29773  supxrnemnf  29884  rexdiv  29982  xrstos  30027  xrge0omnd  30059  cnre2csqlem  30304  fsumcvg4  30344  lmxrge0  30346  qqhval2lem  30373  esumpr2  30477  esumcvg  30496  issgon  30534  measxun2  30621  measres  30633  measdivcstOLD  30635  measdivcst  30636  elorrvc  30873  signsply0  30976  bnj580  31328  erdsze2lem2  31531  cvmsval  31593  fundmpss  32008  dfon2lem3  32032  frmin  32085  poseq  32096  soseq  32097  frrlem5  32127  nosupbnd1  32203  dfrdg4  32401  cgrtriv  32452  btwntriv2  32462  ifscgr  32494  lineext  32526  btwnconn1lem12  32548  colinbtwnle  32568  elicc3  32654  ontgval  32769  onsucconni  32775  bj-bibibi  32908  bj-cbvexw  33001  bj-equsal  33145  bj-restn0  33373  bj-snmoore  33398  bj-elid  33420  bj-finsumval0  33483  relowlssretop  33546  sucneqond  33548  finxpsuc  33570  cnfinltrel  33576  wl-nfs1t  33657  finixpnum  33726  ltflcei  33729  matunitlindflem1  33737  poimirlem23  33764  poimirlem24  33765  poimirlem27  33768  poimirlem32  33773  itg2addnclem  33792  areacirclem2  33832  areacirclem5  33835  areacirc  33836  nninfnub  33877  prdstotbnd  33923  heiborlem4  33943  heibor  33950  elghomlem2OLD  34015  grpokerinj  34022  isidlc  34144  prtlem17  34674  dral1-o  34702  axc16g-o  34732  lsator0sp  34800  atlrelat1  35120  cvratlem  35220  diaintclN  36857  dibintclN  36966  cdlemn11pre  37009  dihord2pre  37024  dihintcl  37143  dochkrshp4  37188  lcfrlem9  37349  lcfrlem21  37362  mapdh8e  37583  elrfirn2  37779  rencldnfilem  37904  sdrgacs  38290  refimssco  38431  rtrclex  38442  intimasn  38467  ss2iundf  38469  ov2ssiunov2  38510  comptiunov2i  38516  iunrelexpuztr  38529  dssmapf1od  38833  snelpwrVD  39578  en3lplem1VD  39590  en3lpVD  39592  orbi1rVD  39595  sbc3orgVD  39598  3impexpVD  39603  equncomVD  39616  trsbcVD  39625  trintALTVD  39628  trintALT  39629  csbingVD  39632  csbsngVD  39641  csbxpgVD  39642  csbrngVD  39644  csbfv12gALTVD  39647  relopabVD  39649  e2ebindVD  39660  xlimbr  40551  stoweidlem35  40749  stoweidlem48  40762  rexrsb  41700  funbrafv  41765  rlimdmafv  41784  tz6.12c-afv2  41849  rlimdmafv2  41865  fzopredsuc  41926  fzoopth  41930  2ffzoeq  41931  iccpartlt  41953  pfxccatin12lem2  42017  proththd  42124  even3prm2  42221  sbgoldbm  42265  nnsum3primesle9  42275  wtgoldbnnsum4prm  42283  bgoldbnnsum3prm  42285  mgm2mgm  42449  2zrngnmlid  42535  2zrngnmrid  42536  ellcoellss  42810  nneop  42906  fldivexpfllog2  42945  digexp  42987  elpglem2  43044
  Copyright terms: Public domain W3C validator