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

Theorem biimpd 230
Description: Deduce an implication from a logical equivalence. Deduction associated with biimp 216 and biimpi 217. (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 216 . 2 ((𝜓𝜒) → (𝜓𝜒))
31, 2syl 17 1 (𝜑 → (𝜓𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207
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 208
This theorem is referenced by:  mpbid  233  sylibd  240  sylbid  241  mpbidi  242  syl5ib  245  syl6bi  254  con4bid  318  mtbird  326  mtbiri  328  imbi1d  343  bitr3  354  pm5.21im  376  biimpa  477  alexbii  1824  spvv  1994  spfw  2031  cbvalw  2033  alcomiwOLD  2042  sbbidvOLD  2076  sbequi  2082  chvarfv  2232  sbbidOLD  2238  cbvalv1  2352  spv  2402  chvar  2404  cbval  2407  sb1  2496  sb4OLD  2499  nfsb4t  2532  nfsb4tALT  2597  exmoeu  2659  euim  2694  2eu3  2732  2eu3OLD  2733  eqrdav  2817  pm13.18  3094  rgen2a  3226  ralcom2w  3360  ralcom2  3361  raleleq  3425  ceqsalgALT  3528  vtoclf  3556  vtocl  3557  vtocl2OLD  3560  spcdv  3590  rspcdv  3612  rspcebdv  3614  rexraleqim  3637  elabgt  3660  sbcn1  3821  sbcim1  3822  sbcbi1  3827  sbeqalb  3833  sbcel21v  3839  elpwunsn  4613  rabsnifsb  4650  ssunsn2  4752  preqr1g  4775  iuneqconst  4921  axprlem3  5316  sbcop1  5370  propeqop  5388  euotd  5394  rexopabb  5406  sotr2  5498  relop  5714  elinxp  5883  elimasni  5949  sotri2  5982  onmindif  6273  iotaval  6322  dffv2  6749  mpteqb  6779  elfvmptrab  6788  chfnrn  6811  elpreima  6820  iinpreima  6829  exfo  6863  ffnfv  6874  f1elima  7012  f1eqcocnv  7048  fliftfun  7054  soisores  7069  isotr  7078  isomin  7079  ovmpodv2  7297  difsnexi  7472  onint  7499  oneqmin  7509  ordunisuc2  7548  tfindsg  7564  findsg  7598  f1oweALT  7662  el2mpocl  7770  ressuppss  7838  funsssuppss  7845  suppofssd  7856  imacosuppOLD  7864  smoiso  7988  seqomlem2  8076  oaordi  8161  oawordri  8165  oaordex  8173  oalimcl  8175  omwordi  8186  oewordi  8206  oelim2  8210  nnmwordi  8250  xpider  8357  iiner  8358  undifixp  8486  mptelixpg  8487  dom2lem  8537  nneneq  8688  fineqvlem  8720  pssnn  8724  dif1en  8739  findcard2s  8747  unfilem2  8771  xpfi  8777  domunfican  8779  f1dmvrnfibi  8796  fsuppimp  8827  dffi2  8875  infsupprpr  8956  wemaplem2  8999  suc11reg  9070  noinfep  9111  cantnflem1  9140  r1fin  9190  tcrank  9301  cardlim  9389  pr2nelem  9418  fseqenlem1  9438  alephnbtwn  9485  alephord2i  9491  alephf1  9499  cardaleph  9503  alephiso  9512  dfac12lem2  9558  ackbij1lem16  9645  cflm  9660  cfcoflem  9682  sornom  9687  fin23lem27  9738  isf32lem7  9769  fin17  9804  fin1a2lem2  9811  fin1a2lem4  9813  fin1a2lem6  9815  fin1a2lem9  9818  axdc3lem2  9861  zorn2lem7  9912  uniimadom  9954  inar1  10185  grothomex  10239  addcanpi  10309  mulcanpi  10310  enqer  10331  genpcd  10416  genpnmax  10417  ltexprlem4  10449  reclem3pr  10459  reclem4pr  10460  suplem2pr  10463  axpre-ltadd  10577  axpre-sup  10579  ltletr  10720  00id  10803  addn0nid  11048  mul0or  11268  prodgt02  11476  lemul1a  11482  mulgt1  11487  divgt0  11496  divge0  11497  ledivp1i  11553  ltdivp1i  11554  cju  11622  nnsub  11669  nominpos  11862  nn0n0n1ge2  11950  btwnnz  12046  suprfinzcl  12085  ublbneg  12321  zmax  12333  cnref1o  12372  ltsubrp  12413  ltaddrp  12414  xrltletr  12538  qbtwnre  12580  xltnegi  12597  xnn0xadd0  12628  iccsupr  12818  icoshft  12847  difreicc  12858  iccshftri  12861  iccshftli  12863  iccdili  12865  icccntri  12867  fzen  12912  elfz1b  12964  fzofzim  13072  eluzgtdifelfzo  13087  elfzo1elm1fzo0  13126  injresinjlem  13145  injresinj  13146  flval2  13172  flval3  13173  modmuladdim  13270  modaddmodup  13290  addmodlteq  13302  fseqsupubi  13334  ssnn0fi  13341  mptnn0fsuppr  13355  sq01  13574  hashf1rn  13701  hashgt12el  13771  hashgt12el2  13772  hash2pr  13815  hash2exprb  13817  hashge2el2difr  13827  hashtpg  13831  hash3tr  13836  lswlgt0cl  13909  ccatalpha  13935  pfxfv  14032  pfxsuff1eqwrdeq  14049  ccatopth2  14067  swrdccat  14085  swrdccat3blem  14089  reuccatpfxs1lem  14096  repsdf2  14128  repswsymball  14129  repswrevw  14137  cshweqrep  14171  cshw1  14172  2cshwcshw  14175  scshwfzeqfzo  14176  cshwcsh2id  14178  swrdco  14187  swrd2lsw  14302  2swrd2eqwrdeq  14303  wwlktovfo  14310  cjre  14486  icodiamlt  14783  reusq0  14810  o1lo1  14882  o1of2  14957  o1rlimmul  14963  zsum  15063  modfsummods  15136  zprod  15279  reeff1  15461  dvdsmod0  15601  dvds2lem  15610  muldvds1  15622  dvdscmulr  15626  dvdsmulcr  15627  dvdsdivcl  15654  mod2eq1n2dvds  15684  oddnn02np1  15685  divalglem8  15739  ndvdsadd  15749  zeqzmulgcd  15847  dfgcd2  15882  gcdmultipleOLD  15888  absproddvds  15949  lcmftp  15968  coprmdvds  15985  2mulprm  16025  isprm5  16039  divgcdodd  16042  isprm6  16046  prmdvdsexpr  16049  cncongrprm  16057  phiprmpw  16101  modprm0  16130  pythagtriplem4  16144  pcz  16205  difsqpwdvds  16211  1arith  16251  prmgaplem5  16379  prmgaplem6  16380  cshwrepswhash1  16424  divsfval  16808  catsubcat  17097  fthmon  17185  isinitoi  17251  istermoi  17252  iszeroi  17257  setcmon  17335  setcepi  17336  funcestrcsetclem8  17385  fthestrcsetc  17388  funcsetcestrclem8  17400  fthsetcestrc  17403  pltnle  17564  pltval3  17565  lublecllem  17586  latasym  17653  odupos  17733  mrelatglb  17782  mrelatlub  17784  cnvpsb  17811  isgrpid2  18078  ghmghmrn  18315  ghmf1  18325  orbsta  18381  resscntz  18400  gsmsymgrfixlem1  18484  gsmsymgreqlem2  18488  mndodcongi  18600  odf1  18618  lsmss1  18720  lsmss2  18722  efgredeu  18807  cntzcmnss  18890  lt6abl  18944  ablfaclem3  19138  ringinvnz1ne0  19271  kerf1ghm  19426  kerf1hrmOLD  19427  lspsneq  19823  lspsneu  19824  lsmcv  19842  lidldvgen  19956  0ringnnzr  19970  domnmuln0  19999  opprdomn  20002  ply1scln0  20387  gsummoncoe1  20400  domnchr  20607  znf1o  20626  zntoslem  20631  znfld  20635  cygznlem2a  20642  cygznlem3  20644  phlssphl  20731  islindf4  20910  uvcendim  20919  matvscl  20968  scmataddcl  21053  scmatsubcl  21054  scmatfo  21067  scmatghm  21070  maducoeval2  21177  slesolinv  21217  cramerimplem2  21221  cpmatelimp  21248  cpmatelimp2  21250  cpmatacl  21252  cpmatinvcl  21253  pm2mpf1  21335  cayhamlem1  21402  cayleyhamilton1  21428  0ntr  21607  islpi  21685  lmss  21834  cmpcld  21938  cmpfi  21944  1stcelcls  21997  comppfsc  22068  ptcnplem  22157  qtophmeo  22353  fbdmn0  22370  fbasrn  22420  elfm3  22486  fmfnfmlem4  22493  fclscf  22561  cnpfcf  22577  alexsubALTlem3  22585  tsmsres  22679  blval2  23099  tnggrpr  23191  nmoleub  23267  nmhmcn  23651  ncvs1  23688  iscau4  23809  caussi  23827  cmssmscld  23880  cmslssbn  23902  cniccbdd  23989  ovoliunnul  24035  mbfinf  24193  itg2splitlem  24276  dvcn  24445  c1lip1  24521  c1lip3  24523  dvcnvrelem1  24541  ply1divex  24657  quotcan  24825  aannenlem1  24844  taylf  24876  ulmcaulem  24909  ulmcau  24910  reeff1o  24962  logccv  25173  logreclem  25267  isosctrlem2  25324  xrlimcnp  25473  rlimcxp  25478  ftalem7  25583  vmappw  25620  fsumvma  25716  dchreq  25761  dchrptlem1  25767  dchrsum  25772  bposlem7  25793  lgsqrlem2  25850  lgsdchr  25858  gausslemma2dlem1a  25868  lgseisenlem2  25879  lgsquad2  25889  2lgslem1b  25895  2sqlem6  25926  2sqnn0  25941  addsq2reu  25943  2sqreulem2  25955  tgcgrcomimp  26190  isperp2  26428  xmstrkgc  26599  brbtwn  26612  brcgr  26613  axcgrid  26629  axeuclidlem  26675  axeuclid  26676  elntg2  26698  lpvtx  26780  upgrex  26804  upgrpredgv  26851  upgredgpr  26854  uhgr0v0e  26947  subgrprop  26982  fusgrfisbase  27037  edgnbusgreu  27076  nbusgredgeu0  27077  cusgredg  27133  structtocusgr  27155  cusgrsize2inds  27162  cusgrsize  27163  usgredgsscusgredg  27168  fusgrmaxsize  27173  uspgrloopvtxel  27225  umgr2v2e  27234  vtxdginducedm1fi  27253  finsumvtxdg2sstep  27258  rgrprop  27269  rusgrprop  27271  0uhgrrusgr  27287  rusgrpropedg  27293  ewlkprop  27312  upgrewlkle2  27315  wlkprop  27320  upgrwlkcompim  27351  uspgr2wlkeq  27354  wlklenvclwlk  27363  wlklenvclwlkOLD  27364  wlkonprop  27367  wlkres  27379  redwlk  27381  wlkdlem2  27392  wksonproplem  27413  usgr2trlspth  27469  usgr2pth  27472  pthdlem1  27474  crctcshwlkn0lem4  27518  wwlksnprcl  27544  wlkiswwlks2  27580  wwlksm1edg  27586  wlknewwlksn  27592  wwlksnred  27597  wwlksnextbi  27599  wwlksnextwrd  27602  wwlksnextinj  27604  wwlksnextsurj  27605  umgr2wlk  27655  umgrwwlks2on  27663  elwwlks2  27672  clwwlk1loop  27693  umgrclwwlkge2  27696  clwlkclwwlklem2a1  27697  clwlkclwwlklem2a4  27702  clwlkclwwlklem2a  27703  clwlkclwwlklem2  27705  clwlkclwwlkfo  27714  clwwisshclwwslemlem  27718  clwwlknwwlksn  27743  clwwlknlbonbgr1  27744  clwwlkn1loopb  27748  clwwlkf  27753  clwwlknon1  27803  clwwlknonwwlknonb  27812  clwwlknonex2lem2  27814  vdn0conngrumgrv2  27902  frgrnbnb  27999  frgrncvvdeqlem2  28006  frgrncvvdeqlem3  28007  frgrncvvdeqlem6  28010  frgrwopreglem4a  28016  fusgr2wsp2nb  28040  frrusgrord0lem  28045  numclwwlk2lem1lem  28048  2clwwlk2clwwlklem  28052  2clwwlk2clwwlk  28056  numclwwlk1lem2foa  28060  numclwwlk1lem2f1  28063  frgrreg  28100  hlipgt0  28618  ocin  29000  ocnel  29002  shmodsi  29093  pjmf1  29420  unopf1o  29620  staddi  29950  stadd3i  29952  mdi  29999  dmdmd  30004  dmdi  30006  dmdbr2  30007  dmdbr3  30009  dmdbr4  30010  dmdi4  30011  mdsl1i  30025  superpos  30058  cvbr4i  30071  atssma  30082  atcv1  30084  atomli  30086  chirredlem1  30094  addltmulALT  30150  bian1d  30151  ifeqeqx  30224  disjxpin  30266  suppss3  30386  fpwrelmap  30395  prmdvdsbc  30458  ogrpaddlt  30645  metider  31033  tpr2rico  31054  xrge0iifiso  31077  qqhcn  31131  qqhucn  31132  esumlub  31218  esumpinfval  31231  esumpinfsum  31235  ballotlemfc0  31649  ballotlemfcc  31650  ftc2re  31768  bnj517  32056  hashfundm  32251  pfxwlk  32267  subgrwlk  32276  loop1cycl  32281  erdsze2lem2  32348  satfv1  32507  satfdmlem  32512  satf0op  32521  fmlasuc  32530  trpredrec  32974  poseq  32992  soseq  32993  sltval2  33060  sltres  33066  nodenselem8  33092  nodense  33093  noresle  33097  scutun12  33168  madeval2  33187  dfrdg4  33309  altopthsn  33319  btwncomim  33371  btwnexch3  33378  btwnexch2  33381  endofsegid  33443  opnrebl2  33566  nn0prpwlem  33567  onsuct0  33686  ordcmp  33692  nndivsub  33702  dnibndlem13  33726  bj-cbval  33879  bj-cbvex  33880  bj-cbvexw  33906  bj-cbv3tb  34006  bj-spimtv  34013  bj-equsal  34046  bj-sbsb  34057  bj-vtoclf  34128  bj-zfauscl  34140  currysetlem2  34156  bj-snsetex  34172  bj-ismooredr2  34296  bj-inftyexpiinj  34383  bj-finsumval0  34455  bj-fvimacnv0  34456  bj-bary1lem1  34480  bj-bary1  34481  f1omptsnlem  34499  iooelexlt  34525  relowlpssretop  34527  rdgeqoa  34533  finxpsuclem  34560  fvineqsneq  34575  pibt2  34580  wl-equsal1i  34664  wl-ax11-lem10  34707  ltflcei  34761  sin2h  34763  cos2h  34764  tan2h  34765  lindsenlbs  34768  matunitlindf  34771  poimirlem3  34776  poimirlem4  34777  poimirlem18  34791  poimirlem20  34793  poimirlem21  34794  poimirlem22  34795  poimirlem24  34797  poimirlem25  34798  poimirlem26  34799  poimirlem27  34800  poimirlem28  34801  poimirlem31  34804  poimir  34806  heicant  34808  mblfinlem1  34810  mblfinlem2  34811  mblfinlem3  34812  mblfinlem4  34813  mbfresfi  34819  cnambfre  34821  ftc1anc  34856  dvasin  34859  areacirclem1  34863  areacirclem4  34866  areacirc  34868  brabg2  34872  fzmul  34897  fdc  34901  incsequz2  34905  isbnd2  34942  opidonOLD  35011  opidon2OLD  35013  grpomndo  35034  elghomlem2OLD  35045  rngoueqz  35099  dvrunz  35113  divrngidl  35187  dral1-o  35920  lsatn0  36015  l1cvpat  36070  leat2  36310  atnle  36333  cvlcvr1  36355  cvrexchlem  36435  cvratlem  36437  cvrat  36438  atcvrj0  36444  atle  36452  snatpsubN  36766  linepsubN  36768  pmapsub  36784  lneq2at  36794  lncvrelatN  36797  2llnma3r  36804  cdlemblem  36809  paddasslem5  36840  poml4N  36969  lhpmcvr4N  37042  trlval2  37179  cdlemd6  37219  cdleme7ga  37264  cdleme25b  37370  cdleme29b  37391  cdleme35fnpq  37465  cdleme50f1  37559  cdlemf1  37577  cdlemg27b  37712  cdlemk28-3  37924  tendospcanN  38039  diaf11N  38065  dia2dimlem1  38080  dibf11N  38177  dihf11  38283  dihmeetlem1N  38306  dochvalr  38373  dochnel2  38408  dvh4dimlem  38459  dochsat0  38473  mapd1o  38664  hdmapf1oN  38881  hgmapval0  38908  hgmapf1oN  38919  hlhilhillem  38976  sn-axprlem3  38987  frlmsnic  39027  oexpreposd  39057  rtprmirr  39072  prjspval  39131  rexrabdioph  39269  fphpdo  39292  irrapxlem3  39299  rmxypairf1o  39386  rmxycomplete  39392  zindbi  39421  lermxnn0  39425  ltrmy  39427  rmyeq0  39428  rmyeq  39429  lermy  39430  acongsym  39451  acongneg2  39452  wepwsolem  39520  intabssd  39763  iscard4  39778  ss2iundf  39882  frege129d  39986  frege133d  39988  axfrege52a  40080  axfrege52c  40111  ntrk0kbimka  40267  gneispace  40362  suprleubrd  40395  suprlubrd  40398  radcnvrat  40523  nzss  40526  expgrowthi  40542  ordpss  40660  bi23impib  40696  bi23imp13  40702  rspsbc2  40745  tratrb  40747  sbcim2g  40749  truniALT  40752  3impcombi  41028  tpid3gVD  41053  orbi1rVD  41059  sbc3orgVD  41062  rspsbc2VD  41066  tratrbVD  41072  sbcim2gVD  41086  sbcbiVD  41087  truniALTVD  41089  trintALTVD  41091  trintALT  41092  csbingVD  41095  csbsngVD  41104  csbxpgVD  41105  csbresgVD  41106  csbrngVD  41107  csbima12gALTVD  41108  csbunigVD  41109  csbfv12gALTVD  41110  relopabVD  41112  isosctrlem1ALT  41145  fzisoeu  41443  xrralrecnnge  41538  allbutfi  41541  climinf  41763  liminfreuzlem  41959  climliminf  41963  climliminflimsup  41965  xlimpnfxnegmnf  41971  xlimbr  41984  stoweidlem7  42169  stoweidlem62  42224  sge0gerpmpt  42561  meaiuninclem  42639  carageniuncllem2  42681  issmflem  42881  funressnfv  43155  funressnvmo  43157  2reu3  43186  ralbinrald  43198  afv0fv0  43225  afv0nbfvbi  43227  afvfv0bi  43228  fnbrafvb  43230  afvres  43248  tz6.12-afv  43249  afvco2  43252  ndmaovcl  43279  afv2res  43315  tz6.12-afv2  43316  nelbrim  43351  f1oresf1o2  43367  zm1nn  43379  nltle2tri  43390  subsubelfzo0  43403  iccpartres  43455  iccpartiltu  43459  fargshiftfv  43476  ichan  43507  ichnreuop  43511  ichreuopeq  43512  prsprel  43526  sprsymrelf1lem  43530  sprsymrelfolem2  43532  sprsymrelfo  43536  prpair  43540  paireqne  43550  sbcpr  43560  fmtnof1  43574  goldbachthlem2  43585  fmtnoprmfac1  43604  fmtnoprmfac2  43606  lighneallem2  43648  lighneallem4b  43651  lighneallem4  43652  evennodd  43685  oddneven  43686  oexpnegnz  43720  evenltle  43759  fpprwppr  43781  fpprwpprb  43782  gbowge7  43805  gbege6  43807  sbgoldbwt  43819  sbgoldbst  43820  nnsum3primesle9  43836  bgoldbtbndlem2  43848  isomuspgrlem1  43869  isomuspgrlem2b  43871  isomuspgrlem2c  43872  isomuspgrlem2d  43873  mgmpropd  43919  clintop  44043  isassintop  44045  lidldomn1  44120  uzlidlring  44128  2zrngnmlid2  44150  rngccatidALTV  44188  ringccatidALTV  44251  srhmsubc  44275  srhmsubcALTV  44293  ztprmneprm  44323  pgrpgt2nabl  44342  lindslinindimp2lem4  44444  lincresunit3  44464  fldivexpfllog2  44553  digexp  44595  affinecomb1  44617  eenglngeehlnmlem1  44652  eenglngeehlnmlem2  44653  eenglngeehlnm  44654  itscnhlc0yqe  44674  itsclc0yqsol  44679  itscnhlc0xyqsol  44680  itschlc0xyqsol1  44681  itschlc0xyqsol  44682  itsclquadeu  44692  inlinecirc02plem  44701  inlinecirc02p  44702  spd  44709  spcdvw  44710  setrec2fun  44723
  Copyright terms: Public domain W3C validator