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  2233  sbbidOLD  2239  cbvalv1  2353  spimtOLD  2398  spv  2405  chvar  2407  cbval  2410  sb1  2499  sb4OLD  2502  nfsb4t  2535  nfsb4tALT  2600  exmoeu  2662  euim  2697  2eu3  2735  2eu3OLD  2736  eqrdav  2820  pm13.18  3097  rgen2a  3229  ralcom2w  3363  ralcom2  3364  raleleq  3428  ceqsalgALT  3531  vtoclf  3559  vtocl  3560  vtocl2OLD  3563  spcdv  3593  rspcdv  3614  rspcebdv  3616  rexraleqim  3639  elabgt  3662  sbcn1  3823  sbcim1  3824  sbcbi1  3829  sbeqalb  3835  sbcel21v  3841  elpwunsn  4615  rabsnifsb  4652  ssunsn2  4754  preqr1g  4777  axprlem3  5317  sbcop1  5371  propeqop  5389  euotd  5395  rexopabb  5407  sotr2  5499  relop  5715  elinxp  5884  elimasni  5950  sotri2  5983  onmindif  6274  iotaval  6323  dffv2  6750  mpteqb  6780  elfvmptrab  6789  chfnrn  6812  elpreima  6821  iinpreima  6830  exfo  6864  ffnfv  6875  f1elima  7012  f1eqcocnv  7048  fliftfun  7054  soisores  7069  isotr  7078  isomin  7079  ovmpodv2  7297  difsnexi  7471  onint  7498  oneqmin  7508  ordunisuc2  7547  tfindsg  7563  findsg  7597  f1oweALT  7664  el2mpocl  7772  ressuppss  7840  funsssuppss  7847  suppofssd  7858  imacosuppOLD  7866  smoiso  7990  seqomlem2  8078  oaordi  8162  oawordri  8166  oaordex  8174  oalimcl  8176  omwordi  8187  oewordi  8207  oelim2  8211  nnmwordi  8251  xpider  8358  iiner  8359  undifixp  8487  mptelixpg  8488  dom2lem  8538  nneneq  8689  fineqvlem  8721  pssnn  8725  dif1en  8740  findcard2s  8748  unfilem2  8772  xpfi  8778  domunfican  8780  f1dmvrnfibi  8797  fsuppimp  8828  dffi2  8876  infsupprpr  8957  wemaplem2  9000  suc11reg  9071  noinfep  9112  cantnflem1  9141  r1fin  9191  tcrank  9302  cardlim  9390  pr2nelem  9419  fseqenlem1  9439  alephnbtwn  9486  alephord2i  9492  alephf1  9500  cardaleph  9504  alephiso  9513  dfac12lem2  9559  ackbij1lem16  9646  cflm  9661  cfcoflem  9683  sornom  9688  fin23lem27  9739  isf32lem7  9770  fin17  9805  fin1a2lem2  9812  fin1a2lem4  9814  fin1a2lem6  9816  fin1a2lem9  9819  axdc3lem2  9862  zorn2lem7  9913  uniimadom  9955  inar1  10186  grothomex  10240  addcanpi  10310  mulcanpi  10311  enqer  10332  genpcd  10417  genpnmax  10418  ltexprlem4  10450  reclem3pr  10460  reclem4pr  10461  suplem2pr  10464  axpre-ltadd  10578  axpre-sup  10580  ltletr  10721  00id  10804  addn0nid  11049  mul0or  11269  prodgt02  11477  lemul1a  11483  mulgt1  11488  divgt0  11497  divge0  11498  ledivp1i  11554  ltdivp1i  11555  cju  11623  nnsub  11670  nominpos  11863  nn0n0n1ge2  11951  btwnnz  12047  suprfinzcl  12086  ublbneg  12322  zmax  12334  cnref1o  12374  ltsubrp  12415  ltaddrp  12416  xrltletr  12540  qbtwnre  12582  xltnegi  12599  xnn0xadd0  12630  iccsupr  12820  icoshft  12849  difreicc  12860  iccshftri  12863  iccshftli  12865  iccdili  12867  icccntri  12869  fzen  12914  elfz1b  12966  fzofzim  13074  eluzgtdifelfzo  13089  elfzo1elm1fzo0  13128  injresinjlem  13147  injresinj  13148  flval2  13174  flval3  13175  modmuladdim  13272  modaddmodup  13292  addmodlteq  13304  fseqsupubi  13336  ssnn0fi  13343  mptnn0fsuppr  13357  sq01  13576  hashf1rn  13703  hashgt12el  13773  hashgt12el2  13774  hash2pr  13817  hash2exprb  13819  hashge2el2difr  13829  hashtpg  13833  hash3tr  13838  lswlgt0cl  13911  ccatalpha  13937  pfxfv  14034  pfxsuff1eqwrdeq  14051  ccatopth2  14069  swrdccat  14087  swrdccat3blem  14091  reuccatpfxs1lem  14098  repsdf2  14130  repswsymball  14131  repswrevw  14139  cshweqrep  14173  cshw1  14174  2cshwcshw  14177  scshwfzeqfzo  14178  cshwcsh2id  14180  swrdco  14189  swrd2lsw  14304  2swrd2eqwrdeq  14305  wwlktovfo  14312  cjre  14488  icodiamlt  14785  reusq0  14812  o1lo1  14884  o1of2  14959  o1rlimmul  14965  zsum  15065  modfsummods  15138  zprod  15281  reeff1  15463  dvdsmod0  15603  dvds2lem  15612  muldvds1  15624  dvdscmulr  15628  dvdsmulcr  15629  dvdsdivcl  15656  mod2eq1n2dvds  15686  oddnn02np1  15687  divalglem8  15741  ndvdsadd  15751  zeqzmulgcd  15849  dfgcd2  15884  gcdmultipleOLD  15890  absproddvds  15951  lcmftp  15970  coprmdvds  15987  2mulprm  16027  isprm5  16041  divgcdodd  16044  isprm6  16048  prmdvdsexpr  16051  cncongrprm  16059  phiprmpw  16103  modprm0  16132  pythagtriplem4  16146  pcz  16207  difsqpwdvds  16213  1arith  16253  prmgaplem5  16381  prmgaplem6  16382  cshwrepswhash1  16426  divsfval  16810  catsubcat  17099  fthmon  17187  isinitoi  17253  istermoi  17254  iszeroi  17259  setcmon  17337  setcepi  17338  funcestrcsetclem8  17387  fthestrcsetc  17390  funcsetcestrclem8  17402  fthsetcestrc  17405  pltnle  17566  pltval3  17567  lublecllem  17588  latasym  17655  odupos  17735  mrelatglb  17784  mrelatlub  17786  cnvpsb  17813  isgrpid2  18080  ghmghmrn  18317  ghmf1  18327  orbsta  18383  resscntz  18402  gsmsymgrfixlem1  18486  gsmsymgreqlem2  18490  mndodcongi  18602  odf1  18620  lsmss1  18722  lsmss2  18724  efgredeu  18809  cntzcmnss  18892  lt6abl  18946  ablfaclem3  19140  ringinvnz1ne0  19273  kerf1ghm  19428  kerf1hrmOLD  19429  lspsneq  19825  lspsneu  19826  lsmcv  19844  lidldvgen  19958  0ringnnzr  19972  domnmuln0  20001  opprdomn  20004  ply1scln0  20389  gsummoncoe1  20402  domnchr  20609  znf1o  20628  zntoslem  20633  znfld  20637  cygznlem2a  20644  cygznlem3  20646  phlssphl  20733  islindf4  20912  uvcendim  20921  matvscl  20970  scmataddcl  21055  scmatsubcl  21056  scmatfo  21069  scmatghm  21072  maducoeval2  21179  slesolinv  21219  cramerimplem2  21223  cpmatelimp  21250  cpmatelimp2  21252  cpmatacl  21254  cpmatinvcl  21255  pm2mpf1  21337  cayhamlem1  21404  cayleyhamilton1  21430  0ntr  21609  islpi  21687  lmss  21836  cmpcld  21940  cmpfi  21946  1stcelcls  21999  comppfsc  22070  ptcnplem  22159  qtophmeo  22355  fbdmn0  22372  fbasrn  22422  elfm3  22488  fmfnfmlem4  22495  fclscf  22563  cnpfcf  22579  alexsubALTlem3  22587  tsmsres  22681  blval2  23101  tnggrpr  23193  nmoleub  23269  nmhmcn  23653  ncvs1  23690  iscau4  23811  caussi  23829  cmssmscld  23882  cmslssbn  23904  cniccbdd  23991  ovoliunnul  24037  mbfinf  24195  itg2splitlem  24278  dvcn  24447  c1lip1  24523  c1lip3  24525  dvcnvrelem1  24543  ply1divex  24659  quotcan  24827  aannenlem1  24846  taylf  24878  ulmcaulem  24911  ulmcau  24912  reeff1o  24964  logccv  25173  logreclem  25267  isosctrlem2  25324  xrlimcnp  25474  rlimcxp  25479  ftalem7  25584  vmappw  25621  fsumvma  25717  dchreq  25762  dchrptlem1  25768  dchrsum  25773  bposlem7  25794  lgsqrlem2  25851  lgsdchr  25859  gausslemma2dlem1a  25869  lgseisenlem2  25880  lgsquad2  25890  2lgslem1b  25896  2sqlem6  25927  2sqnn0  25942  addsq2reu  25944  2sqreulem2  25956  tgcgrcomimp  26191  isperp2  26429  xmstrkgc  26600  brbtwn  26613  brcgr  26614  axcgrid  26630  axeuclidlem  26676  axeuclid  26677  elntg2  26699  lpvtx  26781  upgrex  26805  upgrpredgv  26852  upgredgpr  26855  uhgr0v0e  26948  subgrprop  26983  fusgrfisbase  27038  edgnbusgreu  27077  nbusgredgeu0  27078  cusgredg  27134  structtocusgr  27156  cusgrsize2inds  27163  cusgrsize  27164  usgredgsscusgredg  27169  fusgrmaxsize  27174  uspgrloopvtxel  27226  umgr2v2e  27235  vtxdginducedm1fi  27254  finsumvtxdg2sstep  27259  rgrprop  27270  rusgrprop  27272  0uhgrrusgr  27288  rusgrpropedg  27294  ewlkprop  27313  upgrewlkle2  27316  wlkprop  27321  upgrwlkcompim  27352  uspgr2wlkeq  27355  wlklenvclwlk  27364  wlklenvclwlkOLD  27365  wlkonprop  27368  wlkres  27380  redwlk  27382  wlkdlem2  27393  wksonproplem  27414  usgr2trlspth  27470  usgr2pth  27473  pthdlem1  27475  crctcshwlkn0lem4  27519  wwlksnprcl  27545  wlkiswwlks2  27581  wwlksm1edg  27587  wlknewwlksn  27593  wwlksnred  27598  wwlksnextbi  27600  wwlksnextwrd  27603  wwlksnextinj  27605  wwlksnextsurj  27606  umgr2wlk  27656  umgrwwlks2on  27664  elwwlks2  27673  clwwlk1loop  27694  umgrclwwlkge2  27697  clwlkclwwlklem2a1  27698  clwlkclwwlklem2a4  27703  clwlkclwwlklem2a  27704  clwlkclwwlklem2  27706  clwlkclwwlkfo  27715  clwwisshclwwslemlem  27719  clwwlknwwlksn  27744  clwwlknlbonbgr1  27745  clwwlkn1loopb  27749  clwwlkf  27754  clwwlknon1  27804  clwwlknonwwlknonb  27813  clwwlknonex2lem2  27815  vdn0conngrumgrv2  27903  frgrnbnb  28000  frgrncvvdeqlem2  28007  frgrncvvdeqlem3  28008  frgrncvvdeqlem6  28011  frgrwopreglem4a  28017  fusgr2wsp2nb  28041  frrusgrord0lem  28046  numclwwlk2lem1lem  28049  2clwwlk2clwwlklem  28053  2clwwlk2clwwlk  28057  numclwwlk1lem2foa  28061  numclwwlk1lem2f1  28064  frgrreg  28101  hlipgt0  28619  ocin  29001  ocnel  29003  shmodsi  29094  pjmf1  29421  unopf1o  29621  staddi  29951  stadd3i  29953  mdi  30000  dmdmd  30005  dmdi  30007  dmdbr2  30008  dmdbr3  30010  dmdbr4  30011  dmdi4  30012  mdsl1i  30026  superpos  30059  cvbr4i  30072  atssma  30083  atcv1  30085  atomli  30087  chirredlem1  30095  addltmulALT  30151  bian1d  30152  ifeqeqx  30225  disjxpin  30267  suppss3  30387  fpwrelmap  30396  prmdvdsbc  30459  ogrpaddlt  30646  metider  31034  tpr2rico  31055  xrge0iifiso  31078  qqhcn  31132  qqhucn  31133  esumlub  31219  esumpinfval  31232  esumpinfsum  31236  ballotlemfc0  31650  ballotlemfcc  31651  ftc2re  31769  bnj517  32057  hashfundm  32252  pfxwlk  32268  subgrwlk  32277  loop1cycl  32282  erdsze2lem2  32349  satfv1  32508  satfdmlem  32513  satf0op  32522  fmlasuc  32531  trpredrec  32975  poseq  32993  soseq  32994  sltval2  33061  sltres  33067  nodenselem8  33093  nodense  33094  noresle  33098  scutun12  33169  madeval2  33188  dfrdg4  33310  altopthsn  33320  btwncomim  33372  btwnexch3  33379  btwnexch2  33382  endofsegid  33444  opnrebl2  33567  nn0prpwlem  33568  onsuct0  33687  ordcmp  33693  nndivsub  33703  dnibndlem13  33727  bj-cbval  33880  bj-cbvex  33881  bj-cbvexw  33907  bj-cbv3tb  34007  bj-spimtv  34014  bj-equsal  34047  bj-sbsb  34058  bj-vtoclf  34129  bj-zfauscl  34141  currysetlem2  34157  bj-snsetex  34173  bj-ismooredr2  34297  bj-inftyexpiinj  34384  bj-finsumval0  34456  bj-fvimacnv0  34457  bj-bary1lem1  34481  bj-bary1  34482  f1omptsnlem  34500  iooelexlt  34526  relowlpssretop  34528  rdgeqoa  34534  finxpsuclem  34561  fvineqsneq  34576  pibt2  34581  wl-equsal1i  34665  wl-ax11-lem10  34708  ltflcei  34762  sin2h  34764  cos2h  34765  tan2h  34766  lindsenlbs  34769  matunitlindf  34772  poimirlem3  34777  poimirlem4  34778  poimirlem18  34792  poimirlem20  34794  poimirlem21  34795  poimirlem22  34796  poimirlem24  34798  poimirlem25  34799  poimirlem26  34800  poimirlem27  34801  poimirlem28  34802  poimirlem31  34805  poimir  34807  heicant  34809  mblfinlem1  34811  mblfinlem2  34812  mblfinlem3  34813  mblfinlem4  34814  mbfresfi  34820  cnambfre  34822  ftc1anc  34857  dvasin  34860  areacirclem1  34864  areacirclem4  34867  areacirc  34869  brabg2  34874  fzmul  34899  fdc  34903  incsequz2  34907  isbnd2  34944  opidonOLD  35013  opidon2OLD  35015  grpomndo  35036  elghomlem2OLD  35047  rngoueqz  35101  dvrunz  35115  divrngidl  35189  dral1-o  35922  lsatn0  36017  l1cvpat  36072  leat2  36312  atnle  36335  cvlcvr1  36357  cvrexchlem  36437  cvratlem  36439  cvrat  36440  atcvrj0  36446  atle  36454  snatpsubN  36768  linepsubN  36770  pmapsub  36786  lneq2at  36796  lncvrelatN  36799  2llnma3r  36806  cdlemblem  36811  paddasslem5  36842  poml4N  36971  lhpmcvr4N  37044  trlval2  37181  cdlemd6  37221  cdleme7ga  37266  cdleme25b  37372  cdleme29b  37393  cdleme35fnpq  37467  cdleme50f1  37561  cdlemf1  37579  cdlemg27b  37714  cdlemk28-3  37926  tendospcanN  38041  diaf11N  38067  dia2dimlem1  38082  dibf11N  38179  dihf11  38285  dihmeetlem1N  38308  dochvalr  38375  dochnel2  38410  dvh4dimlem  38461  dochsat0  38475  mapd1o  38666  hdmapf1oN  38883  hgmapval0  38910  hgmapf1oN  38921  hlhilhillem  38978  sn-axprlem3  38989  frlmsnic  39029  oexpreposd  39059  rtprmirr  39074  prjspval  39133  rexrabdioph  39271  fphpdo  39294  irrapxlem3  39301  rmxypairf1o  39388  rmxycomplete  39394  zindbi  39423  lermxnn0  39427  ltrmy  39429  rmyeq0  39430  rmyeq  39431  lermy  39432  acongsym  39453  acongneg2  39454  wepwsolem  39522  intabssd  39765  iscard4  39780  ss2iundf  39884  frege129d  39988  frege133d  39990  axfrege52a  40082  axfrege52c  40113  ntrk0kbimka  40269  gneispace  40364  suprleubrd  40397  suprlubrd  40401  radcnvrat  40526  nzss  40529  expgrowthi  40545  ordpss  40663  bi23impib  40699  bi23imp13  40705  rspsbc2  40748  tratrb  40750  sbcim2g  40752  truniALT  40755  3impcombi  41031  tpid3gVD  41056  orbi1rVD  41062  sbc3orgVD  41065  rspsbc2VD  41069  tratrbVD  41075  sbcim2gVD  41089  sbcbiVD  41090  truniALTVD  41092  trintALTVD  41094  trintALT  41095  csbingVD  41098  csbsngVD  41107  csbxpgVD  41108  csbresgVD  41109  csbrngVD  41110  csbima12gALTVD  41111  csbunigVD  41112  csbfv12gALTVD  41113  relopabVD  41115  isosctrlem1ALT  41148  fzisoeu  41447  xrralrecnnge  41542  allbutfi  41545  climinf  41767  liminfreuzlem  41963  climliminf  41967  climliminflimsup  41969  xlimpnfxnegmnf  41975  xlimbr  41988  stoweidlem7  42173  stoweidlem62  42228  sge0gerpmpt  42565  meaiuninclem  42643  carageniuncllem2  42685  issmflem  42885  funressnfv  43159  funressnvmo  43161  2reu3  43190  ralbinrald  43202  afv0fv0  43229  afv0nbfvbi  43231  afvfv0bi  43232  fnbrafvb  43234  afvres  43252  tz6.12-afv  43253  afvco2  43256  ndmaovcl  43283  afv2res  43319  tz6.12-afv2  43320  nelbrim  43355  f1oresf1o2  43371  zm1nn  43383  nltle2tri  43394  subsubelfzo0  43407  iccpartres  43425  iccpartiltu  43429  fargshiftfv  43446  ichan  43477  ichnreuop  43481  ichreuopeq  43482  prsprel  43496  sprsymrelf1lem  43500  sprsymrelfolem2  43502  sprsymrelfo  43506  prpair  43510  paireqne  43520  sbcpr  43530  fmtnof1  43544  goldbachthlem2  43555  fmtnoprmfac1  43574  fmtnoprmfac2  43576  lighneallem2  43618  lighneallem4b  43621  lighneallem4  43622  evennodd  43655  oddneven  43656  oexpnegnz  43690  evenltle  43729  fpprwppr  43751  fpprwpprb  43752  gbowge7  43775  gbege6  43777  sbgoldbwt  43789  sbgoldbst  43790  nnsum3primesle9  43806  bgoldbtbndlem2  43818  isomuspgrlem1  43839  isomuspgrlem2b  43841  isomuspgrlem2c  43842  isomuspgrlem2d  43843  mgmpropd  43889  clintop  44013  isassintop  44015  lidldomn1  44090  uzlidlring  44098  2zrngnmlid2  44120  rngccatidALTV  44158  ringccatidALTV  44221  srhmsubc  44245  srhmsubcALTV  44263  ztprmneprm  44293  pgrpgt2nabl  44312  lindslinindimp2lem4  44414  lincresunit3  44434  fldivexpfllog2  44523  digexp  44565  affinecomb1  44587  eenglngeehlnmlem1  44622  eenglngeehlnmlem2  44623  eenglngeehlnm  44624  itscnhlc0yqe  44644  itsclc0yqsol  44649  itscnhlc0xyqsol  44650  itschlc0xyqsol1  44651  itschlc0xyqsol  44652  itsclquadeu  44662  inlinecirc02plem  44671  inlinecirc02p  44672  spd  44679  spcdvw  44680  setrec2fun  44693
  Copyright terms: Public domain W3C validator