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

Theorem biimprd 238
 Description: Deduce a converse implication from a logical equivalence. Deduction associated with biimpr 210 and biimpri 218. (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 236 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:  syl6bir  244  mpbird  247  sylibrd  249  sylbird  250  con4bid  306  mtbid  313  mtbii  315  imbi1d  330  biimpar  501  prlem1  1025  alexbii  1800  spfw  2007  spfwOLD  2008  cbvalw  2010  alcomiw  2013  cbvalv1  2211  nfimdOLD  2262  cbval  2307  axc16i  2353  axc16gALT  2395  eqrdav  2650  pm13.18  2904  rspcimdv  3341  rspcedv  3344  moi2  3420  moi  3422  eqrdOLD  3656  sspsstr  3745  eqoreldifOLD  4258  rabsnifsb  4289  ralxfrdOLD  4910  ralxfr2d  4912  isso2i  5096  wefrc  5137  elres  5470  sotri3  5561  oneqmini  5814  ordsssuc2  5852  ordtri2or  5860  2elresin  6040  f1ocnv  6187  tz6.12c  6251  fveqres  6268  fvun1  6308  dffo4  6415  funopsn  6453  fconst5  6512  fnprb  6513  fntpb  6514  isores3  6625  f1owe  6643  weniso  6644  ndmovordi  6867  abnexg  7006  orduniorsuc  7072  ordzsl  7087  tfinds  7101  f1oweALT  7194  fnse  7339  tposfo2  7420  wfrlem5  7464  wfrlem12  7471  issmo2  7491  iordsmo  7499  smoel2  7505  tz7.48lem  7581  oawordeulem  7679  om00  7700  omlimcl  7703  odi  7704  nnawordi  7746  fiint  8278  fipreima  8313  dffi2  8370  suplub2  8408  wemapsolem  8496  unwdomg  8530  inf3lem3  8565  trcl  8642  fidomtri  8857  prdom2  8867  cardaleph  8950  ackbij1lem16  9095  coflim  9121  coftr  9133  infpssrlem4  9166  isfin7-2  9256  axdc3lem2  9311  axdc3lem4  9313  brdom6disj  9392  entric  9417  fpwwe2lem12  9501  inatsk  9638  grur1a  9679  indpi  9767  reclem3pr  9909  supsrlem  9970  lelttr  10166  dedekindle  10239  negn0  10497  fimaxre  11006  nnmulcl  11081  arch  11327  nnnegz  11418  zeo  11501  uzm1  11756  rpneg  11901  xrlttri  12010  xrlelttr  12025  iccid  12258  icoshft  12332  fzen  12396  elfz1b  12447  elfz2nn0  12469  elfzom1p1elfzo  12587  fleqceilz  12693  zmodidfzoimp  12740  modsumfzodifsn  12783  hasheqf1oi  13180  hashnfinnn0  13190  hashle2prv  13298  swrd0  13480  swrdccatin12lem2  13535  swrdccat  13539  swrdccat3blem  13541  repswswrd  13577  trclublem  13780  max0add  14094  abslt  14098  absle  14099  rexuzre  14136  caurcvg  14451  caucvg  14453  dvdsval2  15030  negdvdsb  15045  muldvds2  15054  dvdsabseq  15082  smuval2  15251  smupvallem  15252  rplpwr  15323  alginv  15335  algfx  15340  coprmgcdb  15409  divgcdcoprm0  15426  prmgt1  15456  oddprmgt2  15458  rpexp1i  15480  qnumdencl  15494  phiprmpw  15528  prmdiveq  15538  prm23lt5  15566  pcmpt  15643  infpnlem1  15661  prmgaplem3  15804  prmgaplem8  15809  imasaddfnlem  16235  plelttr  17019  lubval  17031  lublecllem  17035  glbval  17044  mrcmndind  17413  mndodconglem  18006  elfrlmbasn0  20154  mavmulsolcl  20405  slesolex  20536  fvmptnn04if  20702  chfacfisf  20707  chfacfisfcpmat  20708  cnpnei  21116  unconn  21280  comppfsc  21383  kqsat  21582  isr0  21588  qtophmeo  21668  trufil  21761  alexsubALT  21902  cnextcn  21918  ucnima  22132  iducn  22134  bl2in  22252  addcnlem  22714  rescncf  22747  ovoliunlem2  23317  voliun  23368  mbflimsup  23478  itgcn  23654  dvdsq1p  23965  aalioulem2  24133  recosf1o  24326  logrec  24546  xrlimcnp  24740  basellem4  24855  bposlem1  25054  bposlem5  25058  lgsqrmod  25122  lgsdchrval  25124  2lgslem1a1  25159  pntlem3  25343  brbtwn2  25830  axbtwnid  25864  umgredgprv  26047  umgrpredgv  26080  usgredgprvALT  26132  fusgrfisstep  26266  fusgrfis  26267  nbupgr  26285  nbumgrvtx  26287  finsumvtxdg2size  26502  wlkp1lem8  26633  upgr2pthnlp  26684  wwlksnextinj  26862  usgr2wspthons3  26931  clwlkclwwlklem2a1  26958  clwwisshclwws  26972  clwwlknonex2lem2  27083  eucrctshift  27221  eucrct2eupth  27223  numclwwlk2lem1  27356  numclwwlk2lem1OLD  27363  numclwwlk5lem  27374  frgrreggt1  27380  frgrreg  27381  friendship  27386  blocn2  27791  htthlem  27902  axhcompl-zf  27983  spanuni  28531  spansncol  28555  spansneleq  28557  elspansn5  28561  idcnop  28968  pjnormssi  29155  dmdmd  29287  bian1d  29434  ifeqeqx  29487  opabssi  29551  supxrnemnf  29662  rexdiv  29762  xrstos  29807  xrge0omnd  29839  cnre2csqlem  30084  fsumcvg4  30124  lmxrge0  30126  qqhval2lem  30153  esumpr2  30257  esumcvg  30276  issgon  30314  measxun2  30401  measres  30413  measdivcstOLD  30415  measdivcst  30416  elorrvc  30653  signsply0  30756  bnj580  31109  erdsze2lem2  31312  cvmsval  31374  fundmpss  31790  dfon2lem3  31814  frmin  31867  poseq  31878  soseq  31879  frrlem5  31909  nosupbnd1  31985  dfrdg4  32183  cgrtriv  32234  btwntriv2  32244  ifscgr  32276  lineext  32308  btwnconn1lem12  32330  colinbtwnle  32350  elicc3  32436  ontgval  32555  onsucconni  32561  bj-bibibi  32696  bj-cbvexw  32789  bj-equsal  32938  bj-restn0  33168  bj-snmoore  33193  bj-elid  33215  bj-finsumval0  33277  relowlssretop  33341  sucneqond  33343  finxpsuc  33365  wl-nfs1t  33454  finixpnum  33524  ltflcei  33527  matunitlindflem1  33535  poimirlem23  33562  poimirlem24  33563  poimirlem27  33566  poimirlem32  33571  itg2addnclem  33591  areacirclem2  33631  areacirclem5  33634  areacirc  33635  nninfnub  33677  prdstotbnd  33723  heiborlem4  33743  heibor  33750  elghomlem2OLD  33815  grpokerinj  33822  isidlc  33944  prtlem17  34480  dral1-o  34508  axc16g-o  34538  lsator0sp  34606  atlrelat1  34926  cvratlem  35025  diaintclN  36664  dibintclN  36773  cdlemn11pre  36816  dihord2pre  36831  dihintcl  36950  dochkrshp4  36995  lcfrlem9  37156  lcfrlem21  37169  mapdh8e  37390  elrfirn2  37576  rencldnfilem  37701  sdrgacs  38088  refimssco  38230  rtrclex  38241  intimasn  38266  ss2iundf  38268  ov2ssiunov2  38309  comptiunov2i  38315  iunrelexpuztr  38328  dssmapf1od  38632  snelpwrVD  39380  en3lplem1VD  39392  en3lpVD  39394  orbi1rVD  39397  sbc3orgVD  39400  3impexpVD  39405  equncomVD  39418  trsbcVD  39427  trintALTVD  39430  trintALT  39431  csbingVD  39434  csbsngVD  39443  csbxpgVD  39444  csbrngVD  39446  csbfv12gALTVD  39449  relopabVD  39451  e2ebindVD  39462  xlimbr  40371  stoweidlem35  40570  stoweidlem48  40583  rexrsb  41490  funbrafv  41559  rlimdmafv  41578  fzopredsuc  41658  fzoopth  41662  2ffzoeq  41663  iccpartlt  41685  pfxccatin12lem2  41749  proththd  41856  even3prm2  41953  sbgoldbm  41997  nnsum3primesle9  42007  wtgoldbnnsum4prm  42015  bgoldbnnsum3prm  42017  mgm2mgm  42188  2zrngnmlid  42274  2zrngnmrid  42275  ellcoellss  42549  nneop  42645  fldivexpfllog2  42684  digexp  42726  elpglem2  42783
 Copyright terms: Public domain W3C validator