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

Theorem biimpd 232
Description: Deduce an implication from a logical equivalence. Deduction associated with biimp 218 and biimpi 219. (Contributed by NM, 11-Jan-1993.)
Hypothesis
Ref Expression
biimpd.1 (𝜑 → (𝜓𝜒))
Assertion
Ref Expression
biimpd (𝜑 → (𝜓𝜒))

Proof of Theorem biimpd
StepHypRef Expression
1 biimpd.1 . 2 (𝜑 → (𝜓𝜒))
2 biimp 218 . 2 ((𝜓𝜒) → (𝜓𝜒))
31, 2syl 17 1 (𝜑 → (𝜓𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209
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 210
This theorem is referenced by:  mpbid  235  sylibd  242  sylbid  243  mpbidi  244  syl5ib  247  syl6bi  256  con4bid  320  mtbird  328  mtbiri  330  imbi1d  345  bitr3  356  pm5.21im  378  biimpa  480  alexbii  1834  spvv  2004  spfw  2041  cbvalw  2043  alcomiwOLD  2052  sbbidvOLD  2086  sbequi  2092  chvarfv  2244  sbbidOLD  2250  cbvalv1  2363  spv  2413  chvar  2415  cbval  2418  sb1  2505  sb4OLD  2508  nfsb4t  2541  nfsb4tALT  2606  exmoeu  2667  euim  2704  2eu3  2741  eqrdav  2823  pm13.18  3095  rgen2a  3223  ralcom2  3354  raleleq  3410  ceqsalgALT  3516  vtoclf  3544  vtocl2OLD  3548  spcdv  3579  rspcdv  3601  rspcebdv  3603  rexraleqim  3626  elabgt  3647  sbcn1  3809  sbcim1  3810  sbcbi1  3815  sbeqalb  3821  sbcel21v  3826  elpwunsn  4606  rabsnifsb  4643  ssunsn2  4744  preqr1g  4767  iuneqconst  4916  axprlem3  5313  sbcop1  5366  propeqop  5384  euotd  5390  rexopabb  5402  sotr2  5492  relop  5708  elinxp  5877  elimasni  5943  sotri2  5976  onmindif  6267  iotaval  6317  dffv2  6747  mpteqb  6778  elfvmptrab  6787  chfnrn  6810  elpreima  6819  iinpreima  6828  exfo  6862  ffnfv  6873  f1elima  7013  f1eqcocnv  7049  f1eqcocnvOLD  7050  fliftfun  7058  soisores  7073  isotr  7082  isomin  7083  ovmpodv2  7301  difsnexi  7477  onint  7504  oneqmin  7514  ordunisuc2  7553  tfindsg  7569  findsg  7604  f1oweALT  7668  el2mpocl  7777  ressuppss  7845  funsssuppss  7852  suppofssd  7863  imacosuppOLD  7871  smoiso  7995  seqomlem2  8083  oaordi  8168  oawordri  8172  oaordex  8180  oalimcl  8182  omwordi  8193  oewordi  8213  oelim2  8217  nnmwordi  8257  xpider  8364  iiner  8365  undifixp  8494  mptelixpg  8495  dom2lem  8545  nneneq  8697  fineqvlem  8729  pssnn  8733  dif1en  8748  findcard2s  8756  unfilem2  8780  xpfi  8786  domunfican  8788  f1dmvrnfibi  8805  fsuppimp  8836  dffi2  8884  infsupprpr  8965  wemaplem2  9008  suc11reg  9079  noinfep  9120  cantnflem1  9149  r1fin  9199  tcrank  9310  cardlim  9398  pr2nelem  9428  fseqenlem1  9448  alephnbtwn  9495  alephord2i  9501  alephf1  9509  cardaleph  9513  alephiso  9522  dfac12lem2  9568  ackbij1lem16  9655  cflm  9670  cfcoflem  9692  sornom  9697  fin23lem27  9748  isf32lem7  9779  fin17  9814  fin1a2lem2  9821  fin1a2lem4  9823  fin1a2lem6  9825  fin1a2lem9  9828  axdc3lem2  9871  zorn2lem7  9922  uniimadom  9964  inar1  10195  grothomex  10249  addcanpi  10319  mulcanpi  10320  enqer  10341  genpcd  10426  genpnmax  10427  ltexprlem4  10459  reclem3pr  10469  reclem4pr  10470  suplem2pr  10473  axpre-ltadd  10587  axpre-sup  10589  ltletr  10730  00id  10813  addn0nid  11058  mul0or  11278  prodgt02  11486  lemul1a  11492  mulgt1  11497  divgt0  11506  divge0  11507  ledivp1i  11563  ltdivp1i  11564  cju  11630  nnsub  11678  nominpos  11871  nn0n0n1ge2  11959  btwnnz  12055  suprfinzcl  12094  ublbneg  12330  zmax  12342  cnref1o  12381  ltsubrp  12422  ltaddrp  12423  xrltletr  12547  qbtwnre  12589  xltnegi  12606  xnn0xadd0  12637  iccsupr  12829  icoshft  12860  difreicc  12871  iccshftri  12874  iccshftli  12876  iccdili  12878  icccntri  12880  fzen  12928  elfz1b  12980  fzofzim  13088  eluzgtdifelfzo  13103  elfzo1elm1fzo0  13142  injresinjlem  13161  injresinj  13162  flval2  13188  flval3  13189  modmuladdim  13286  modaddmodup  13306  addmodlteq  13318  fseqsupubi  13350  ssnn0fi  13357  mptnn0fsuppr  13371  sq01  13591  hashf1rn  13718  hashgt12el  13788  hashgt12el2  13789  hash2pr  13832  hash2exprb  13834  hashge2el2difr  13844  hashtpg  13848  hash3tr  13853  lswlgt0cl  13921  ccatalpha  13947  pfxfv  14044  pfxsuff1eqwrdeq  14061  ccatopth2  14079  swrdccat  14097  swrdccat3blem  14101  reuccatpfxs1lem  14108  repsdf2  14140  repswsymball  14141  repswrevw  14149  cshweqrep  14183  cshw1  14184  2cshwcshw  14187  scshwfzeqfzo  14188  cshwcsh2id  14190  swrdco  14199  swrd2lsw  14314  2swrd2eqwrdeq  14315  wwlktovfo  14322  cjre  14498  icodiamlt  14795  reusq0  14822  o1lo1  14894  o1of2  14969  o1rlimmul  14975  zsum  15075  modfsummods  15148  zprod  15291  reeff1  15473  dvdsmod0  15613  dvds2lem  15622  muldvds1  15634  dvdscmulr  15638  dvdsmulcr  15639  dvdsdivcl  15666  mod2eq1n2dvds  15696  oddnn02np1  15697  divalglem8  15749  ndvdsadd  15759  zeqzmulgcd  15857  dfgcd2  15892  gcdmultipleOLD  15898  absproddvds  15959  lcmftp  15978  coprmdvds  15995  2mulprm  16035  isprm5  16049  divgcdodd  16052  isprm6  16056  prmdvdsexpr  16059  cncongrprm  16067  phiprmpw  16111  modprm0  16140  pythagtriplem4  16154  pcz  16215  difsqpwdvds  16221  1arith  16261  prmgaplem5  16389  prmgaplem6  16390  cshwrepswhash1  16436  divsfval  16820  catsubcat  17109  fthmon  17197  isinitoi  17263  istermoi  17264  iszeroi  17269  setcmon  17347  setcepi  17348  funcestrcsetclem8  17397  fthestrcsetc  17400  funcsetcestrclem8  17412  fthsetcestrc  17415  pltnle  17576  pltval3  17577  lublecllem  17598  latasym  17665  odupos  17745  mrelatglb  17794  mrelatlub  17796  cnvpsb  17823  isgrpid2  18140  ghmghmrn  18377  ghmf1  18387  orbsta  18443  resscntz  18462  gsmsymgrfixlem1  18555  gsmsymgreqlem2  18559  mndodcongi  18671  odf1  18689  lsmss1  18791  lsmss2  18793  efgredeu  18878  cntzcmnss  18961  lt6abl  19015  ablfaclem3  19209  ringinvnz1ne0  19345  kerf1ghm  19498  lspsneq  19894  lspsneu  19895  lsmcv  19913  lidldvgen  20028  0ringnnzr  20042  domnmuln0  20071  opprdomn  20074  ply1scln0  20459  gsummoncoe1  20472  domnchr  20679  znf1o  20698  zntoslem  20703  znfld  20707  cygznlem2a  20714  cygznlem3  20716  phlssphl  20803  islindf4  20982  uvcendim  20991  matvscl  21040  scmataddcl  21125  scmatsubcl  21126  scmatfo  21139  scmatghm  21142  maducoeval2  21249  slesolinv  21289  cramerimplem2  21293  cpmatelimp  21320  cpmatelimp2  21322  cpmatacl  21324  cpmatinvcl  21325  pm2mpf1  21407  cayhamlem1  21474  cayleyhamilton1  21500  0ntr  21679  islpi  21757  lmss  21906  cmpcld  22010  cmpfi  22016  1stcelcls  22069  comppfsc  22140  ptcnplem  22229  qtophmeo  22425  fbdmn0  22442  fbasrn  22492  elfm3  22558  fmfnfmlem4  22565  fclscf  22633  cnpfcf  22649  alexsubALTlem3  22657  tsmsres  22752  blval2  23172  tnggrpr  23264  nmoleub  23340  nmhmcn  23728  ncvs1  23765  iscau4  23886  caussi  23904  cmssmscld  23957  cmslssbn  23979  cniccbdd  24068  ovoliunnul  24114  mbfinf  24272  itg2splitlem  24355  dvcn  24527  c1lip1  24603  c1lip3  24605  dvcnvrelem1  24623  ply1divex  24740  quotcan  24908  aannenlem1  24927  taylf  24959  ulmcaulem  24992  ulmcau  24993  reeff1o  25045  logccv  25257  logreclem  25351  isosctrlem2  25408  xrlimcnp  25557  rlimcxp  25562  ftalem7  25667  vmappw  25704  fsumvma  25800  dchreq  25845  dchrptlem1  25851  dchrsum  25856  bposlem7  25877  lgsqrlem2  25934  lgsdchr  25942  gausslemma2dlem1a  25952  lgseisenlem2  25963  lgsquad2  25973  2lgslem1b  25979  2sqlem6  26010  2sqnn0  26025  addsq2reu  26027  2sqreulem2  26039  tgcgrcomimp  26274  isperp2  26512  xmstrkgc  26683  brbtwn  26696  brcgr  26697  axcgrid  26713  axeuclidlem  26759  axeuclid  26760  elntg2  26782  lpvtx  26864  upgrex  26888  upgrpredgv  26935  upgredgpr  26938  uhgr0v0e  27031  subgrprop  27066  fusgrfisbase  27121  edgnbusgreu  27160  nbusgredgeu0  27161  cusgredg  27217  structtocusgr  27239  cusgrsize2inds  27246  cusgrsize  27247  usgredgsscusgredg  27252  fusgrmaxsize  27257  uspgrloopvtxel  27309  umgr2v2e  27318  vtxdginducedm1fi  27337  finsumvtxdg2sstep  27342  rgrprop  27353  rusgrprop  27355  0uhgrrusgr  27371  rusgrpropedg  27377  ewlkprop  27396  upgrewlkle2  27399  wlkprop  27404  upgrwlkcompim  27435  uspgr2wlkeq  27438  wlklenvclwlk  27447  wlklenvclwlkOLD  27448  wlkonprop  27451  wlkres  27463  redwlk  27465  wlkdlem2  27476  wksonproplem  27497  usgr2trlspth  27553  usgr2pth  27556  pthdlem1  27558  crctcshwlkn0lem4  27602  wwlksnprcl  27628  wlkiswwlks2  27664  wwlksm1edg  27670  wlknewwlksn  27676  wwlksnred  27681  wwlksnextbi  27683  wwlksnextwrd  27686  wwlksnextinj  27688  wwlksnextsurj  27689  umgr2wlk  27738  umgrwwlks2on  27746  elwwlks2  27755  clwwlk1loop  27776  umgrclwwlkge2  27779  clwlkclwwlklem2a1  27780  clwlkclwwlklem2a4  27785  clwlkclwwlklem2a  27786  clwlkclwwlklem2  27788  clwlkclwwlkfo  27797  clwwisshclwwslemlem  27801  clwwlknwwlksn  27826  clwwlknlbonbgr1  27827  clwwlkn1loopb  27831  clwwlkf  27835  clwwlknon1  27885  clwwlknonwwlknonb  27894  clwwlknonex2lem2  27896  vdn0conngrumgrv2  27984  frgrnbnb  28081  frgrncvvdeqlem2  28088  frgrncvvdeqlem3  28089  frgrncvvdeqlem6  28092  frgrwopreglem4a  28098  fusgr2wsp2nb  28122  frrusgrord0lem  28127  numclwwlk2lem1lem  28130  2clwwlk2clwwlklem  28134  2clwwlk2clwwlk  28138  numclwwlk1lem2foa  28142  numclwwlk1lem2f1  28145  frgrreg  28182  hlipgt0  28700  ocin  29082  ocnel  29084  shmodsi  29175  pjmf1  29502  unopf1o  29702  staddi  30032  stadd3i  30034  mdi  30081  dmdmd  30086  dmdi  30088  dmdbr2  30089  dmdbr3  30091  dmdbr4  30092  dmdi4  30093  mdsl1i  30107  superpos  30140  cvbr4i  30153  atssma  30164  atcv1  30166  atomli  30168  chirredlem1  30176  addltmulALT  30232  bian1d  30233  ifeqeqx  30308  disjxpin  30349  suppss3  30471  fpwrelmap  30480  prmdvdsbc  30543  ogrpaddlt  30750  metider  31194  tpr2rico  31212  xrge0iifiso  31235  qqhcn  31289  qqhucn  31290  esumlub  31376  esumpinfval  31389  esumpinfsum  31393  ballotlemfc0  31807  ballotlemfcc  31808  ftc2re  31926  bnj517  32214  hashfundm  32411  pfxwlk  32427  subgrwlk  32436  loop1cycl  32441  erdsze2lem2  32508  satfv1  32667  satfdmlem  32672  satf0op  32681  fmlasuc  32690  trpredrec  33134  poseq  33152  soseq  33153  sltval2  33220  sltres  33226  nodenselem8  33252  nodense  33253  noresle  33257  scutun12  33328  madeval2  33347  dfrdg4  33469  altopthsn  33479  btwncomim  33531  btwnexch3  33538  btwnexch2  33541  endofsegid  33603  opnrebl2  33726  nn0prpwlem  33727  onsuct0  33846  ordcmp  33852  nndivsub  33862  dnibndlem13  33886  bj-cbval  34039  bj-cbvex  34040  bj-cbvexw  34066  bj-cbv3tb  34168  bj-spimtv  34175  bj-equsal  34208  bj-sbsb  34219  bj-vtoclf  34299  bj-zfauscl  34311  currysetlem2  34327  bj-snsetex  34343  bj-ismooredr2  34470  bj-inftyexpiinj  34569  bj-finsumval0  34645  bj-fvimacnv0  34646  bj-bary1lem1  34670  bj-bary1  34671  f1omptsnlem  34698  iooelexlt  34724  relowlpssretop  34726  rdgeqoa  34732  finxpsuclem  34759  fvineqsneq  34774  pibt2  34779  wl-equsal1i  34893  wl-ax11-lem10  34936  ltflcei  34990  sin2h  34992  cos2h  34993  tan2h  34994  lindsenlbs  34997  matunitlindf  35000  poimirlem3  35005  poimirlem4  35006  poimirlem18  35020  poimirlem20  35022  poimirlem21  35023  poimirlem22  35024  poimirlem24  35026  poimirlem25  35027  poimirlem26  35028  poimirlem27  35029  poimirlem28  35030  poimirlem31  35033  poimir  35035  heicant  35037  mblfinlem1  35039  mblfinlem2  35040  mblfinlem3  35041  mblfinlem4  35042  mbfresfi  35048  cnambfre  35050  ftc1anc  35083  dvasin  35086  areacirclem1  35090  areacirclem4  35093  areacirc  35095  brabg2  35099  fzmul  35124  fdc  35128  incsequz2  35132  isbnd2  35166  opidonOLD  35235  opidon2OLD  35237  grpomndo  35258  elghomlem2OLD  35269  rngoueqz  35323  dvrunz  35337  divrngidl  35411  dral1-o  36145  lsatn0  36240  l1cvpat  36295  leat2  36535  atnle  36558  cvlcvr1  36580  cvrexchlem  36660  cvratlem  36662  cvrat  36663  atcvrj0  36669  atle  36677  snatpsubN  36991  linepsubN  36993  pmapsub  37009  lneq2at  37019  lncvrelatN  37022  2llnma3r  37029  cdlemblem  37034  paddasslem5  37065  poml4N  37194  lhpmcvr4N  37267  trlval2  37404  cdlemd6  37444  cdleme7ga  37489  cdleme25b  37595  cdleme29b  37616  cdleme35fnpq  37690  cdleme50f1  37784  cdlemf1  37802  cdlemg27b  37937  cdlemk28-3  38149  tendospcanN  38264  diaf11N  38290  dia2dimlem1  38305  dibf11N  38402  dihf11  38508  dihmeetlem1N  38531  dochvalr  38598  dochnel2  38633  dvh4dimlem  38684  dochsat0  38698  mapd1o  38889  hdmapf1oN  39106  hgmapval0  39133  hgmapf1oN  39144  hlhilhillem  39201  nnproddivdvdsd  39237  lcmineqlem  39288  metakunt7  39302  sn-axprlem3  39337  frlmsnic  39387  oexpreposd  39417  rtprmirr  39432  prjspval  39513  rexrabdioph  39651  fphpdo  39674  irrapxlem3  39681  rmxypairf1o  39768  rmxycomplete  39774  zindbi  39803  lermxnn0  39807  ltrmy  39809  rmyeq0  39810  rmyeq  39811  lermy  39812  acongsym  39833  acongneg2  39834  wepwsolem  39902  intabssd  40143  iscard4  40157  ss2iundf  40276  frege129d  40380  frege133d  40382  axfrege52a  40474  axfrege52c  40505  ntrk0kbimka  40661  gneispace  40756  suprleubrd  40789  suprlubrd  40792  radcnvrat  40938  nzss  40941  expgrowthi  40957  ordpss  41075  bi23impib  41111  bi23imp13  41117  rspsbc2  41160  tratrb  41162  sbcim2g  41164  truniALT  41167  3impcombi  41443  tpid3gVD  41468  orbi1rVD  41474  sbc3orgVD  41477  rspsbc2VD  41481  tratrbVD  41487  sbcim2gVD  41501  sbcbiVD  41502  truniALTVD  41504  trintALTVD  41506  trintALT  41507  csbingVD  41510  csbsngVD  41519  csbxpgVD  41520  csbresgVD  41521  csbrngVD  41522  csbima12gALTVD  41523  csbunigVD  41524  csbfv12gALTVD  41525  relopabVD  41527  isosctrlem1ALT  41560  fzisoeu  41858  xrralrecnnge  41952  allbutfi  41955  climinf  42174  liminfreuzlem  42370  climliminf  42374  climliminflimsup  42376  xlimpnfxnegmnf  42382  xlimbr  42395  stoweidlem7  42575  stoweidlem62  42630  sge0gerpmpt  42967  meaiuninclem  43045  carageniuncllem2  43087  issmflem  43287  funressnfv  43561  funressnvmo  43563  2reu3  43592  ralbinrald  43604  afv0fv0  43631  afv0nbfvbi  43633  afvfv0bi  43634  fnbrafvb  43636  afvres  43654  tz6.12-afv  43655  afvco2  43658  ndmaovcl  43685  afv2res  43721  tz6.12-afv2  43722  nelbrim  43757  f1oresf1o2  43773  zm1nn  43785  nltle2tri  43796  subsubelfzo0  43809  iccpartres  43861  iccpartiltu  43865  fargshiftfv  43882  ichnreuop  43915  ichreuopeq  43916  prsprel  43930  sprsymrelf1lem  43934  sprsymrelfolem2  43936  sprsymrelfo  43940  prpair  43944  paireqne  43954  sbcpr  43964  fmtnof1  43978  goldbachthlem2  43989  fmtnoprmfac1  44008  fmtnoprmfac2  44010  lighneallem2  44050  lighneallem4b  44053  lighneallem4  44054  evennodd  44087  oddneven  44088  oexpnegnz  44122  evenltle  44161  fpprwppr  44183  fpprwpprb  44184  gbowge7  44207  gbege6  44209  sbgoldbwt  44221  sbgoldbst  44222  nnsum3primesle9  44238  bgoldbtbndlem2  44250  isomuspgrlem1  44271  isomuspgrlem2b  44273  isomuspgrlem2c  44274  isomuspgrlem2d  44275  mgmpropd  44321  clintop  44394  isassintop  44396  lidldomn1  44471  uzlidlring  44479  2zrngnmlid2  44501  rngccatidALTV  44539  ringccatidALTV  44602  srhmsubc  44626  srhmsubcALTV  44644  ztprmneprm  44675  pgrpgt2nabl  44694  lindslinindimp2lem4  44796  lincresunit3  44816  fldivexpfllog2  44905  digexp  44947  naryfvalelfv  44972  affinecomb1  45042  eenglngeehlnmlem1  45077  eenglngeehlnmlem2  45078  eenglngeehlnm  45079  itscnhlc0yqe  45099  itsclc0yqsol  45104  itscnhlc0xyqsol  45105  itschlc0xyqsol1  45106  itschlc0xyqsol  45107  itsclquadeu  45117  inlinecirc02plem  45126  inlinecirc02p  45127  spd  45134  spcdvw  45135  setrec2fun  45148
  Copyright terms: Public domain W3C validator