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

Theorem biimpd 219
Description: Deduce an implication from a logical equivalence. Deduction associated with biimp 205 and biimpi 206. (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 205 . 2 ((𝜓𝜒) → (𝜓𝜒))
31, 2syl 17 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:  mpbid  222  sylibd  229  sylbid  230  mpbidi  231  syl5ib  234  syl6bi  243  ibi  256  con4bid  306  mtbird  314  mtbiri  316  imbi1d  330  bitr3  341  pm5.21im  363  biimpa  500  alexbii  1800  exintr  1859  spfw  2007  spfwOLD  2008  cbvalw  2010  alcomiw  2013  stdpc5OLD  2115  cbvalv1  2211  spimt  2289  spv  2296  chvar  2298  cbval  2307  nfsb4t  2417  2eu3  2584  eqrdav  2650  rgen2a  3006  ralcom2  3133  raleleq  3186  ceqsalgALT  3262  vtoclf  3289  vtocl  3290  vtocl2  3292  vtocl3  3293  spcdv  3322  rspcdv  3343  rspcebdv  3345  rexraleqim  3359  elabgt  3379  sbcn1  3514  sbcim1  3515  sbcbi1  3516  sbeqalb  3521  sbcel21v  3530  eqrdOLD  3656  elpwunsn  4256  rabsnifsb  4289  ssunsn2  4391  preqr1g  4416  propeqop  4999  euotd  5004  sotr2  5093  relop  5305  elres  5470  restidsingOLD  5494  elimasni  5527  sotri2  5560  relcnvtr  5693  onmindif  5853  iotaval  5900  dffv2  6310  mpteqb  6338  elfvmptrab  6345  chfnrn  6368  elpreima  6377  iinpreima  6385  exfo  6417  ffnfv  6428  f1elima  6560  f1eqcocnv  6596  fliftfun  6602  soisores  6617  isotr  6626  isomin  6627  ovmpt2dv2  6836  difsnexi  7012  onint  7037  oneqmin  7047  ordunisuc2  7086  tfindsg  7102  findsg  7135  f1oweALT  7194  el2mpt2cl  7296  ressuppss  7359  funsssuppss  7366  imacosupp  7380  smoiso  7504  seqomlem2  7591  oaordi  7671  oawordri  7675  oaordex  7683  oalimcl  7685  omwordi  7696  oewordi  7716  oelim2  7720  nnmwordi  7760  xpider  7861  iiner  7862  undifixp  7986  mptelixpg  7987  dom2lem  8037  nneneq  8184  fineqvlem  8215  pssnn  8219  dif1en  8234  findcard2s  8242  unfilem2  8266  xpfi  8272  domunfican  8274  f1dmvrnfibi  8291  fsuppimp  8322  dffi2  8370  wemaplem2  8493  suc11reg  8554  noinfep  8595  cantnflem1  8624  r1fin  8674  tcrank  8785  cardlim  8836  pr2nelem  8865  fseqenlem1  8885  alephnbtwn  8932  alephord2i  8938  alephf1  8946  cardaleph  8950  alephiso  8959  dfac12lem2  9004  ackbij1lem16  9095  cflm  9110  cfcoflem  9132  sornom  9137  fin23lem27  9188  isf32lem7  9219  fin17  9254  fin1a2lem2  9261  fin1a2lem4  9263  fin1a2lem6  9265  fin1a2lem9  9268  axdc3lem2  9311  zorn2lem7  9362  uniimadom  9404  inar1  9635  grothomex  9689  addcanpi  9759  mulcanpi  9760  enqer  9781  genpcd  9866  genpnmax  9867  ltexprlem4  9899  reclem3pr  9909  reclem4pr  9910  suplem2pr  9913  axpre-ltadd  10026  axpre-sup  10028  ltletr  10167  00id  10249  addn0nid  10489  mul0or  10705  prodgt02  10907  prodge02  10909  lemul1a  10915  mulgt1  10920  divgt0  10929  divge0  10930  ledivp1i  10987  ltdivp1i  10988  cju  11054  nnsub  11097  nominpos  11307  nn0n0n1ge2  11396  btwnnz  11491  suprfinzcl  11530  ublbneg  11811  zmax  11823  cnref1o  11865  ltsubrp  11904  ltaddrp  11905  xrltletr  12026  qbtwnre  12068  xltnegi  12085  xnn0xadd0  12115  iccsupr  12304  icoshft  12332  difreicc  12342  iccshftri  12345  iccshftli  12347  iccdili  12349  icccntri  12351  fzen  12396  elfz1b  12447  fzofzim  12554  eluzgtdifelfzo  12569  elfzo1elm1fzo0  12609  injresinjlem  12628  injresinj  12629  flval2  12655  flval3  12656  modmuladdim  12753  modaddmodup  12773  addmodlteq  12785  fseqsupubi  12817  ssnn0fi  12824  mptnn0fsuppr  12839  sq01  13026  hashf1rn  13181  hashgt12el  13248  hashgt12el2  13249  hash2pr  13289  hash2exprb  13291  hashge2el2difr  13301  hashtpg  13305  hash3tr  13310  lswlgt0cl  13389  ccatalpha  13411  2swrd1eqwrdeq  13500  ccatopth2  13517  reuccats1lem  13525  swrdccatin2  13533  swrdccat  13539  swrdccat3a  13540  swrdccat3blem  13541  repsdf2  13571  repswsymball  13572  repswrevw  13579  cshweqrep  13613  cshw1  13614  2cshwcshw  13617  scshwfzeqfzo  13618  cshwcsh2id  13620  swrdco  13629  swrd2lsw  13741  2swrd2eqwrdeq  13742  wwlktovfo  13747  cjre  13923  icodiamlt  14218  o1lo1  14312  o1of2  14387  o1rlimmul  14393  zsum  14493  modfsummods  14569  zprod  14711  reeff1  14894  dvdsmod0  15033  dvds2lem  15041  muldvds1  15053  dvdscmulr  15057  dvdsmulcr  15058  dvdsdivcl  15085  mod2eq1n2dvds  15118  oddnn02np1  15119  divalglem8  15170  ndvdsadd  15181  zeqzmulgcd  15279  dfgcd2  15310  gcdmultiple  15316  absproddvds  15377  lcmftp  15396  coprmdvds  15413  isprm5  15466  divgcdodd  15469  isprm6  15473  prmdvdsexpr  15476  cncongrprm  15484  phiprmpw  15528  modprm0  15557  pythagtriplem4  15571  pcz  15632  difsqpwdvds  15638  1arith  15678  prmgaplem5  15806  prmgaplem6  15807  cshwrepswhash1  15856  divsfval  16254  catsubcat  16546  fthmon  16634  isinitoi  16700  istermoi  16701  iszeroi  16706  setcmon  16784  setcepi  16785  funcestrcsetclem8  16834  fthestrcsetc  16837  funcsetcestrclem8  16849  fthsetcestrc  16852  pltnle  17013  pltval3  17014  lublecllem  17035  latasym  17102  odupos  17182  mrelatglb  17231  mrelatlub  17233  cnvpsb  17260  isgrpid2  17505  ghmghmrn  17726  ghmf1  17736  orbsta  17792  resscntz  17810  gsmsymgrfixlem1  17893  gsmsymgreqlem2  17897  mndodcongi  18008  odf1  18025  lsmss1  18125  lsmss2  18127  efgredeu  18211  cntzcmnss  18292  lt6abl  18342  ablfaclem3  18532  ringinvnz1ne0  18638  kerf1hrm  18791  lspsneq  19170  lspsneu  19171  lsmcv  19189  lidldvgen  19303  0ringnnzr  19317  domnmuln0  19346  opprdomn  19349  ply1scln0  19709  gsummoncoe1  19722  domnchr  19928  znf1o  19948  zntoslem  19953  znfld  19957  cygznlem2a  19964  cygznlem3  19966  islindf4  20225  uvcendim  20234  matvscl  20285  scmataddcl  20370  scmatsubcl  20371  scmatfo  20384  scmatghm  20387  maducoeval2  20494  slesolinv  20534  cramerimplem2  20538  cpmatelimp  20565  cpmatelimp2  20567  cpmatacl  20569  cpmatinvcl  20570  pm2mpf1  20652  cayhamlem1  20719  cayleyhamilton1  20745  0ntr  20923  islpi  21001  lmss  21150  cmpcld  21253  cmpfi  21259  1stcelcls  21312  comppfsc  21383  ptcnplem  21472  qtophmeo  21668  fbdmn0  21685  fbasrn  21735  elfm3  21801  fmfnfmlem4  21808  fclscf  21876  cnpfcf  21892  alexsubALTlem3  21900  tsmsres  21994  blval2  22414  tnggrpr  22506  nmoleub  22582  nmhmcn  22966  ncvs1  23003  iscau4  23123  caussi  23141  cniccbdd  23276  ovoliunnul  23321  mbfinf  23477  itg2splitlem  23560  dvcn  23729  c1lip1  23805  c1lip3  23807  dvcnvrelem1  23825  ply1divex  23941  quotcan  24109  aannenlem1  24128  taylf  24160  ulmcaulem  24193  ulmcau  24194  reeff1o  24246  logccv  24454  logreclem  24545  isosctrlem2  24594  xrlimcnp  24740  rlimcxp  24745  ftalem7  24850  vmappw  24887  fsumvma  24983  dchreq  25028  dchrptlem1  25034  dchrsum  25039  bposlem7  25060  lgsqrlem2  25117  lgsdchr  25125  gausslemma2dlem1a  25135  lgseisenlem2  25146  lgsquad2  25156  2lgslem1b  25162  2sqlem6  25193  tgcgrcomimp  25417  isperp2  25655  xmstrkgc  25811  brbtwn  25824  brcgr  25825  axcgrid  25841  axeuclidlem  25887  axeuclid  25888  lpvtx  26008  upgrex  26032  upgrpredgv  26079  upgredgpr  26082  uhgr0v0e  26175  subgrprop  26210  fusgrfisbase  26265  edgnbusgreu  26313  nbusgredgeu0  26314  cusgredg  26376  structtocusgr  26398  cusgrsize2inds  26405  cusgrsize  26406  usgredgsscusgredg  26411  fusgrmaxsize  26416  uspgrloopvtxel  26468  umgr2v2e  26477  vtxdginducedm1fi  26496  finsumvtxdg2sstep  26501  rgrprop  26512  rusgrprop  26514  0uhgrrusgr  26530  rusgrpropedg  26536  ewlkprop  26555  upgrewlkle2  26558  wlkprop  26563  upgrwlkcompim  26595  uspgr2wlkeq  26598  wlklenvclwlk  26607  wlkonprop  26610  wlkres  26623  redwlk  26625  wlkdlem2  26636  wksonproplem  26657  usgr2trlspth  26713  usgr2pth  26716  pthdlem1  26718  crctcshwlkn0lem4  26761  wwlksnprcl  26787  wlkiswwlks2  26829  wwlksm1edg  26835  wlknewwlksn  26841  wwlksnred  26855  wwlksnext  26856  wwlksnextbi  26857  wwlksnextwrd  26860  wwlksnextinj  26862  wwlksnextsur  26863  umgr2wlk  26914  umgrwwlks2on  26923  elwwlks2  26933  clwwlk1loop  26956  umgrclwwlkge2  26957  clwlkclwwlklem2a1  26958  clwlkclwwlklem2a4  26963  clwlkclwwlklem2a  26964  clwlkclwwlklem2  26966  clwwisshclwwslemlem  26970  clwwlknwwlksn  27000  clwwlknwwlksnOLD  27001  clwwlknlbonbgr1  27002  clwwlkn1loopb  27006  clwwlkf  27010  wwlksext2clwwlk  27021  wwlksext2clwwlkOLD  27022  clwlksfclwwlk  27049  clwwlknon1  27072  clwwlknonwwlknonb  27080  clwwlknonwwlknonbOLD  27081  clwwlknonex2lem2  27083  vdn0conngrumgrv2  27174  frgrnbnb  27273  frgrncvvdeqlem2  27280  frgrncvvdeqlem3  27281  frgrncvvdeqlem6  27284  frgrwopreglem4a  27290  fusgr2wsp2nb  27314  frrusgrord0lem  27319  numclwwlk2lem1lem  27324  numclwwlk2lem1lemOLD  27325  2clwwlk2clwwlklem2lem2  27329  clwwlkccatlem  27331  2clwwlk2clwwlk  27338  numclwlk1lem2foa  27344  numclwlk1lem2f1  27347  frgrreg  27381  hlipgt0  27898  ocin  28283  ocnel  28285  shmodsi  28376  pjmf1  28703  unopf1o  28903  staddi  29233  stadd3i  29235  mdi  29282  dmdmd  29287  dmdi  29289  dmdbr2  29290  dmdbr3  29292  dmdbr4  29293  dmdi4  29294  mdsl1i  29308  superpos  29341  cvbr4i  29354  atssma  29365  atcv1  29367  atomli  29369  chirredlem1  29377  addltmulALT  29433  bian1d  29434  ifeqeqx  29487  disjxpin  29527  suppss3  29630  fpwrelmap  29636  ogrpaddlt  29846  metider  30065  tpr2rico  30086  xrge0iifiso  30109  qqhcn  30163  qqhucn  30164  esumlub  30250  esumpinfval  30263  esumpinfsum  30267  ballotlemfc0  30682  ballotlemfcc  30683  ftc2re  30804  bnj517  31081  erdsze2lem2  31312  trpredrec  31862  poseq  31878  soseq  31879  sltval2  31934  sltres  31940  nodenselem8  31966  nodense  31967  noresle  31971  scutun12  32042  madeval2  32061  dfrdg4  32183  altopthsn  32193  btwncomim  32245  btwnexch3  32252  btwnexch2  32255  endofsegid  32317  opnrebl2  32441  nn0prpwlem  32442  onsuct0  32565  ordcmp  32571  nndivsub  32581  dnibndlem13  32605  bj-cbvexw  32789  bj-cbv3tb  32836  bj-spimtv  32843  bj-spvv  32848  bj-chvarv  32850  bj-equsal  32938  bj-sbsb  32949  bj-ax8  33012  bj-vtoclf  33033  bj-snsetex  33076  bj-ismooredr2  33190  bj-inftyexpiinj  33226  bj-finsumval0  33277  bj-bary1lem1  33291  bj-bary1  33292  f1omptsnlem  33313  iooelexlt  33340  relowlpssretop  33342  rdgeqoa  33348  finxpsuclem  33364  wl-equsal1i  33459  wl-ax11-lem10  33501  ltflcei  33527  sin2h  33529  cos2h  33530  tan2h  33531  lindsenlbs  33534  matunitlindf  33537  poimirlem3  33542  poimirlem4  33543  poimirlem18  33557  poimirlem20  33559  poimirlem21  33560  poimirlem22  33561  poimirlem24  33563  poimirlem25  33564  poimirlem26  33565  poimirlem27  33566  poimirlem28  33567  poimirlem31  33570  poimir  33572  heicant  33574  mblfinlem1  33576  mblfinlem2  33577  mblfinlem3  33578  mblfinlem4  33579  mbfresfi  33586  cnambfre  33588  ftc1anc  33623  dvasin  33626  areacirclem1  33630  areacirclem4  33633  areacirc  33635  brabg2  33640  fzmul  33667  fdc  33671  incsequz2  33675  isbnd2  33712  opidonOLD  33781  opidon2OLD  33783  grpomndo  33804  elghomlem2OLD  33815  rngoueqz  33869  dvrunz  33883  divrngidl  33957  dral1-o  34508  lsatn0  34604  l1cvpat  34659  leat2  34899  atnle  34922  cvlcvr1  34944  cvrexchlem  35023  cvratlem  35025  cvrat  35026  atcvrj0  35032  atle  35040  snatpsubN  35354  linepsubN  35356  pmapsub  35372  lneq2at  35382  lncvrelatN  35385  2llnma3r  35392  cdlemblem  35397  paddasslem5  35428  poml4N  35557  lhpmcvr4N  35630  trlval2  35768  cdlemd6  35808  cdleme7ga  35853  cdleme25b  35959  cdleme29b  35980  cdleme35fnpq  36054  cdleme50f1  36148  cdlemf1  36166  cdlemg27b  36301  cdlemk28-3  36513  tendospcanN  36629  diaf11N  36655  dia2dimlem1  36670  dibf11N  36767  dihf11  36873  dihmeetlem1N  36896  dochvalr  36963  dochnel2  36998  dvh4dimlem  37049  dochsat0  37063  mapd1o  37254  hdmapf1oN  37474  hgmapval0  37501  hgmapf1oN  37512  hlhilhillem  37569  rexrabdioph  37675  fphpdo  37698  irrapxlem3  37705  rmxypairf1o  37793  rmxycomplete  37799  zindbi  37828  lermxnn0  37834  ltrmy  37836  rmyeq0  37837  rmyeq  37838  lermy  37839  acongsym  37860  acongneg2  37861  wepwsolem  37929  intabssd  38233  ss2iundf  38268  frege129d  38372  frege133d  38374  axfrege52a  38467  axfrege52c  38498  ntrk0kbimka  38654  gneispace  38749  suprleubrd  38783  suprlubrd  38787  radcnvrat  38830  nzss  38833  expgrowthi  38849  ordpss  38972  bi23impib  39008  bi23imp13  39014  rspsbc2  39061  tratrb  39063  sbcim2g  39065  truniALT  39068  3impcombi  39361  tpid3gVD  39391  orbi1rVD  39397  sbc3orgVD  39400  rspsbc2VD  39404  tratrbVD  39411  sbcim2gVD  39425  sbcbiVD  39426  truniALTVD  39428  trintALTVD  39430  trintALT  39431  csbingVD  39434  csbsngVD  39443  csbxpgVD  39444  csbresgVD  39445  csbrngVD  39446  csbima12gALTVD  39447  csbunigVD  39448  csbfv12gALTVD  39449  relopabVD  39451  isosctrlem1ALT  39484  fzisoeu  39828  xrralrecnnge  39926  allbutfi  39929  climinf  40156  liminfreuzlem  40352  climliminf  40356  climliminflimsup  40358  xlimbr  40371  stoweidlem7  40542  stoweidlem62  40597  sge0gerpmpt  40937  meaiuninclem  41015  carageniuncllem2  41057  issmflem  41257  2reu3  41509  ralbinrald  41520  funressnfv  41529  afv0fv0  41550  afv0nbfvbi  41552  afvfv0bi  41553  fnbrafvb  41555  afvres  41573  tz6.12-afv  41574  afvco2  41577  ndmaovcl  41604  nelbrim  41616  zm1nn  41641  nltle2tri  41648  subsubelfzo0  41661  iccpartres  41679  iccpartiltu  41683  fargshiftfv  41700  pfxfv  41724  pfxsuff1eqwrdeq  41732  reuccatpfxs1lem  41758  fmtnof1  41772  goldbachthlem2  41783  fmtnoprmfac1  41802  fmtnoprmfac2  41804  lighneallem2  41848  lighneallem4b  41851  lighneallem4  41852  evennodd  41881  oddneven  41882  oexpnegALTV  41913  oexpnegnz  41914  evenltle  41951  gbowge7  41976  gbege6  41978  sbgoldbwt  41990  sbgoldbst  41991  nnsum3primesle9  42007  bgoldbtbndlem2  42019  prsprel  42062  sprsymrelf1lem  42066  sprsymrelfolem2  42068  sprsymrelfo  42072  mgmpropd  42100  clintop  42169  isassintop  42171  lidldomn1  42246  uzlidlring  42254  2zrngnmlid2  42276  rngccatidALTV  42314  ringccatidALTV  42377  srhmsubc  42401  srhmsubcALTV  42419  ztprmneprm  42450  pgrpgt2nabl  42472  lindslinindimp2lem4  42575  lincresunit3  42595  fldivexpfllog2  42684  digexp  42726  spd  42750  spcdvw  42751  setrec2fun  42764
  Copyright terms: Public domain W3C validator