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  307  mtbird  315  mtbiri  317  imbi1d  331  bitr3  342  pm5.21im  364  biimpa  501  alexbii  1757  exintr  1816  spfw  1962  spfwOLD  1963  cbvalw  1965  alcomiw  1968  stdpc5OLD  2075  cbvalv1  2174  spimt  2252  spv  2259  chvar  2261  cbval  2270  nfsb4t  2388  2eu3  2554  eqrdav  2620  rgen2a  2973  ralcom2  3098  raleleq  3149  ceqsalgALT  3221  vtoclf  3248  vtocl  3249  vtocl2  3251  vtocl3  3252  spcdv  3281  rspcdv  3302  rexraleqim  3317  elabgt  3335  sbcn1  3468  sbcim1  3469  sbcbi1  3470  sbeqalb  3475  sbcel21v  3484  eqrdOLD  3608  elpwunsn  4202  rabsnifsb  4234  ssunsn2  4334  preqr1g  4360  propeqop  4940  euotd  4945  sotr2  5034  relop  5242  elres  5404  restidsingOLD  5428  elimasni  5461  sotri2  5494  relcnvtr  5624  onmindif  5784  iotaval  5831  dffv2  6238  mpteqb  6265  elfvmptrab  6272  chfnrn  6294  elpreima  6303  iinpreima  6311  exfo  6343  ffnfv  6354  f1elima  6485  f1eqcocnv  6521  fliftfun  6527  soisores  6542  isotr  6551  isomin  6552  ovmpt2dv2  6759  difsnexi  6934  onint  6957  oneqmin  6967  ordunisuc2  7006  tfindsg  7022  findsg  7055  f1oweALT  7112  el2mpt2cl  7211  ressuppss  7274  funsssuppss  7281  imacosupp  7295  smoiso  7419  seqomlem2  7506  oaordi  7586  oawordri  7590  oaordex  7598  oalimcl  7600  omwordi  7611  oewordi  7631  oelim2  7635  nnmwordi  7675  xpider  7778  iiner  7779  undifixp  7904  mptelixpg  7905  dom2lem  7955  nneneq  8103  fineqvlem  8134  pssnn  8138  dif1en  8153  findcard2s  8161  unfilem2  8185  xpfi  8191  domunfican  8193  f1dmvrnfibi  8210  fsuppimp  8241  dffi2  8289  wemaplem2  8412  suc11reg  8476  noinfep  8517  cantnflem1  8546  r1fin  8596  tcrank  8707  cardlim  8758  pr2nelem  8787  fseqenlem1  8807  alephnbtwn  8854  alephord2i  8860  alephf1  8868  cardaleph  8872  alephiso  8881  dfac12lem2  8926  ackbij1lem16  9017  cflm  9032  cfcoflem  9054  sornom  9059  fin23lem27  9110  isf32lem7  9141  fin17  9176  fin1a2lem2  9183  fin1a2lem4  9185  fin1a2lem6  9187  fin1a2lem9  9190  axdc3lem2  9233  zorn2lem7  9284  uniimadom  9326  inar1  9557  grothomex  9611  addcanpi  9681  mulcanpi  9682  enqer  9703  genpcd  9788  genpnmax  9789  ltexprlem4  9821  reclem3pr  9831  reclem4pr  9832  suplem2pr  9835  axpre-ltadd  9948  axpre-sup  9950  ltletr  10089  00id  10171  addn0nid  10411  mul0or  10627  prodgt02  10829  prodge02  10831  lemul1a  10837  mulgt1  10842  divgt0  10851  divge0  10852  ledivp1i  10909  ltdivp1i  10910  cju  10976  nnsub  11019  nominpos  11229  nn0n0n1ge2  11318  btwnnz  11413  suprfinzcl  11452  ublbneg  11733  zmax  11745  cnref1o  11787  ltsubrp  11826  ltaddrp  11827  xrltletr  11948  qbtwnre  11989  xltnegi  12006  xnn0xadd0  12036  iccsupr  12224  icoshft  12252  difreicc  12262  iccshftri  12265  iccshftli  12267  iccdili  12269  icccntri  12271  fzen  12316  fzofzim  12471  eluzgtdifelfzo  12486  elfzo1elm1fzo0  12526  injresinjlem  12544  injresinj  12545  flval2  12571  flval3  12572  modmuladdim  12669  modaddmodup  12689  addmodlteq  12701  fseqsupubi  12733  ssnn0fi  12740  mptnn0fsuppr  12755  sq01  12942  hashf1rn  13098  hashf1rnOLD  13099  hashgt12el  13166  hashgt12el2  13167  hash2pr  13205  hash2exprb  13207  hashge2el2difr  13217  hashtpg  13221  hash3tr  13227  lswlgt0cl  13311  ccatalpha  13330  2swrd1eqwrdeq  13408  ccatopth2  13425  reuccats1lem  13433  swrdccatin2  13440  swrdccat  13446  swrdccat3a  13447  swrdccat3blem  13448  repsdf2  13478  repswsymball  13479  repswrevw  13486  cshweqrep  13520  cshw1  13521  2cshwcshw  13524  scshwfzeqfzo  13525  cshwcsh2id  13527  swrdco  13536  swrd2lsw  13645  2swrd2eqwrdeq  13646  wwlktovfo  13651  cjre  13829  icodiamlt  14124  o1lo1  14218  o1of2  14293  o1rlimmul  14299  zsum  14398  modfsummods  14471  zprod  14611  reeff1  14794  dvds2lem  14937  muldvds1  14949  dvdscmulr  14953  dvdsmulcr  14954  dvdsdivcl  14981  mod2eq1n2dvds  15014  oddnn02np1  15015  divalglem8  15066  ndvdsadd  15077  zeqzmulgcd  15175  dfgcd2  15206  gcdmultiple  15212  absproddvds  15273  lcmftp  15292  coprmdvds  15309  isprm5  15362  divgcdodd  15365  isprm6  15369  prmdvdsexpr  15372  cncongrprm  15380  phiprmpw  15424  modprm0  15453  pythagtriplem4  15467  pcz  15528  difsqpwdvds  15534  1arith  15574  prmgaplem5  15702  prmgaplem6  15703  cshwrepswhash1  15752  divsfval  16147  catsubcat  16439  fthmon  16527  isinitoi  16593  istermoi  16594  iszeroi  16599  setcmon  16677  setcepi  16678  funcestrcsetclem8  16727  fthestrcsetc  16730  funcsetcestrclem8  16742  fthsetcestrc  16745  pltnle  16906  pltval3  16907  lublecllem  16928  latasym  16995  odupos  17075  mrelatglb  17124  mrelatlub  17126  cnvpsb  17153  isgrpid2  17398  ghmghmrn  17619  ghmf1  17629  orbsta  17686  resscntz  17704  gsmsymgrfixlem1  17787  gsmsymgreqlem2  17791  mndodcongi  17902  odf1  17919  lsmss1  18019  lsmss2  18021  efgredeu  18105  cntzcmnss  18186  lt6abl  18236  ablfaclem3  18426  ringinvnz1ne0  18532  kerf1hrm  18683  lspsneq  19062  lspsneu  19063  lsmcv  19081  lidldvgen  19195  0ringnnzr  19209  domnmuln0  19238  opprdomn  19241  ply1scln0  19601  gsummoncoe1  19614  domnchr  19820  znf1o  19840  zntoslem  19845  znfld  19849  cygznlem2a  19856  cygznlem3  19858  islindf4  20117  uvcendim  20126  matvscl  20177  scmataddcl  20262  scmatsubcl  20263  scmatfo  20276  scmatghm  20279  maducoeval2  20386  slesolinv  20426  cramerimplem2  20430  cpmatelimp  20457  cpmatelimp2  20459  cpmatacl  20461  cpmatinvcl  20462  pm2mpf1  20544  cayhamlem1  20611  cayleyhamilton1  20637  0ntr  20815  islpi  20893  lmss  21042  cmpcld  21145  cmpfi  21151  1stcelcls  21204  comppfsc  21275  ptcnplem  21364  qtophmeo  21560  fbdmn0  21578  fbasrn  21628  elfm3  21694  fmfnfmlem4  21701  fclscf  21769  cnpfcf  21785  alexsubALTlem3  21793  tsmsres  21887  blval2  22307  tnggrpr  22399  nmoleub  22475  nmhmcn  22860  ncvs1  22897  iscau4  23017  caussi  23035  cniccbdd  23170  ovoliunnul  23215  mbfinf  23372  itg2splitlem  23455  dvcn  23624  c1lip1  23698  c1lip3  23700  dvcnvrelem1  23718  ply1divex  23834  quotcan  24002  aannenlem1  24021  taylf  24053  ulmcaulem  24086  ulmcau  24087  reeff1o  24139  logccv  24343  logreclem  24434  isosctrlem2  24483  xrlimcnp  24629  rlimcxp  24634  ftalem7  24739  vmappw  24776  fsumvma  24872  dchreq  24917  dchrptlem1  24923  dchrsum  24928  bposlem7  24949  lgsqrlem2  25006  lgsdchr  25014  gausslemma2dlem1a  25024  lgseisenlem2  25035  lgsquad2  25045  2lgslem1b  25051  2sqlem6  25082  tgcgrcomimp  25306  isperp2  25544  xmstrkgc  25700  brbtwn  25713  brcgr  25714  axcgrid  25730  axeuclidlem  25776  axeuclid  25777  lpvtx  25893  upgrex  25917  upgrpredgv  25963  upgredgpr  25966  uhgr0v0e  26057  subgrprop  26092  fusgrfisbase  26142  edgnbusgreu  26190  nbusgredgeu0  26191  cusgredg  26241  structtocusgr  26263  cusgrsize2inds  26270  cusgrsize  26271  usgredgsscusgredg  26276  fusgrmaxsize  26281  uspgrloopvtxel  26332  umgr2v2e  26341  rgrprop  26360  rusgrprop  26362  0uhgrrusgr  26378  rusgrpropedg  26384  ewlkprop  26403  upgrewlkle2  26406  wlkprop  26411  upgrwlkcompim  26442  uspgr2wlkeq  26445  wlklenvclwlk  26454  wlkonprop  26457  wlkres  26470  redwlk  26472  wlkdlem2  26483  wksonproplem  26504  usgr2trlspth  26560  usgr2pth  26563  pthdlem1  26565  crctcshwlkn0lem4  26608  wspthnonp  26647  wlkiswwlks2  26664  wwlksm1edg  26670  wlknewwlksn  26676  wwlksnred  26690  wwlksnext  26691  wwlksnextbi  26692  wwlksnextwrd  26695  wwlksnextinj  26697  wwlksnextsur  26698  umgr2wlk  26748  umgrwwlks2on  26753  elwspths2on  26755  usgr2wspthons3  26759  elwwlks2  26762  clwwlknp  26788  clwlkclwwlklem2a1  26794  clwlkclwwlklem2a4  26799  clwlkclwwlklem2a  26800  clwlkclwwlklem2  26802  clwwlks1loop  26808  umgrclwwlksge2  26812  clwwlksf  26815  wwlksext2clwwlk  26824  clwwisshclwwslemlem  26826  clwwnisshclwwsn  26830  clwlksfclwwlk  26862  vdn0conngrumgrv2  26956  frgrnbnb  27055  frgrncvvdeqlem3  27063  frgrncvvdeqlem4  27064  frgrncvvdeqlem7  27067  frgrwopreg  27078  fusgr2wsp2nb  27090  frrusgrord0  27095  clwwlkextfrlem1  27101  numclwwlkovf2ex  27109  numclwlk1lem2foa  27113  numclwwlk8  27138  frgrreg  27140  hlipgt0  27658  ocin  28043  ocnel  28045  shmodsi  28136  pjmf1  28463  unopf1o  28663  staddi  28993  stadd3i  28995  mdi  29042  dmdmd  29047  dmdi  29049  dmdbr2  29050  dmdbr3  29052  dmdbr4  29053  dmdi4  29054  mdsl1i  29068  superpos  29101  cvbr4i  29114  atssma  29125  atcv1  29127  atomli  29129  chirredlem1  29137  addltmulALT  29193  bian1d  29194  ifeqeqx  29249  disjxpin  29287  suppss3  29386  fpwrelmap  29392  ogrpaddlt  29545  metider  29761  tpr2rico  29782  xrge0iifiso  29805  qqhcn  29859  qqhucn  29860  esumlub  29945  esumpinfval  29958  esumpinfsum  29962  ballotlemfc0  30377  ballotlemfcc  30378  ftc2re  30492  bnj517  30716  erdsze2lem2  30947  trpredrec  31492  poseq  31504  soseq  31505  sltval2  31563  sltres  31571  slttr3  31589  nodenselem7  31603  nodenselem8  31604  nodense  31605  nobndup  31616  nobnddown  31617  dfrdg4  31753  altopthsn  31763  btwncomim  31815  btwnexch3  31822  btwnexch2  31825  endofsegid  31887  opnrebl2  32011  nn0prpwlem  32012  onsuct0  32135  ordcmp  32141  nndivsub  32151  dnibndlem13  32175  bj-cbvexw  32359  bj-cbv3tb  32406  bj-spimtv  32413  bj-spvv  32418  bj-chvarv  32420  bj-equsal  32509  bj-sbsb  32520  bj-ax8  32587  bj-vtoclf  32608  bj-snsetex  32651  bj-inftyexpiinj  32768  bj-finsumval0  32819  bj-bary1lem1  32833  bj-bary1  32834  f1omptsnlem  32854  iooelexlt  32881  relowlpssretop  32883  rdgeqoa  32889  finxpsuclem  32905  wl-equsal1i  33000  wl-ax11-lem10  33042  ltflcei  33068  sin2h  33070  cos2h  33071  tan2h  33072  lindsenlbs  33075  matunitlindf  33078  poimirlem3  33083  poimirlem4  33084  poimirlem18  33098  poimirlem20  33100  poimirlem21  33101  poimirlem22  33102  poimirlem24  33104  poimirlem25  33105  poimirlem26  33106  poimirlem27  33107  poimirlem28  33108  poimirlem31  33111  poimir  33113  heicant  33115  mblfinlem1  33117  mblfinlem2  33118  mblfinlem3  33119  mblfinlem4  33120  mbfresfi  33127  cnambfre  33129  ftc1anc  33164  dvasin  33167  areacirclem1  33171  areacirclem4  33174  areacirc  33176  brabg2  33181  fzmul  33208  fdc  33212  incsequz2  33216  isbnd2  33253  opidonOLD  33322  opidon2OLD  33324  grpomndo  33345  elghomlem2OLD  33356  rngoueqz  33410  dvrunz  33424  divrngidl  33498  dral1-o  33708  lsatn0  33805  l1cvpat  33860  leat2  34100  atnle  34123  cvlcvr1  34145  cvrexchlem  34224  cvratlem  34226  cvrat  34227  atcvrj0  34233  atle  34241  snatpsubN  34555  linepsubN  34557  pmapsub  34573  lneq2at  34583  lncvrelatN  34586  2llnma3r  34593  cdlemblem  34598  paddasslem5  34629  poml4N  34758  lhpmcvr4N  34831  trlval2  34969  cdlemd6  35009  cdleme7ga  35054  cdleme25b  35161  cdleme29b  35182  cdleme35fnpq  35256  cdleme50f1  35350  cdlemf1  35368  cdlemg27b  35503  cdlemk28-3  35715  tendospcanN  35831  diaf11N  35857  dia2dimlem1  35872  dibf11N  35969  dihf11  36075  dihmeetlem1N  36098  dochvalr  36165  dochnel2  36200  dvh4dimlem  36251  dochsat0  36265  mapd1o  36456  hdmapf1oN  36676  hgmapval0  36703  hgmapf1oN  36714  hlhilhillem  36771  rexrabdioph  36877  fphpdo  36900  irrapxlem3  36907  rmxypairf1o  36995  rmxycomplete  37001  zindbi  37030  lermxnn0  37036  ltrmy  37038  rmyeq0  37039  rmyeq  37040  lermy  37041  acongsym  37062  acongneg2  37063  wepwsolem  37131  intabssd  37436  ss2iundf  37471  frege129d  37575  frege133d  37577  axfrege52a  37671  axfrege52c  37702  ntrk0kbimka  37858  gneispace  37953  suprleubrd  37987  suprlubrd  37991  radcnvrat  38034  nzss  38037  expgrowthi  38053  ordpss  38176  bi23impib  38212  bi23imp13  38218  rspsbc2  38265  tratrb  38267  sbcim2g  38269  truniALT  38272  3impcombi  38565  tpid3gVD  38599  orbi1rVD  38605  sbc3orgVD  38608  rspsbc2VD  38612  tratrbVD  38619  sbcim2gVD  38633  sbcbiVD  38634  truniALTVD  38636  trintALTVD  38638  trintALT  38639  csbingVD  38642  csbsngVD  38651  csbxpgVD  38652  csbresgVD  38653  csbrngVD  38654  csbima12gALTVD  38655  csbunigVD  38656  csbfv12gALTVD  38657  relopabVD  38659  isosctrlem1ALT  38692  fzisoeu  39013  xrralrecnnge  39112  allbutfi  39115  climinf  39274  stoweidlem7  39561  stoweidlem62  39616  sge0gerpmpt  39956  meaiuninclem  40034  carageniuncllem2  40073  issmflem  40273  2reu3  40522  ralbinrald  40533  funressnfv  40542  afv0fv0  40563  afv0nbfvbi  40565  afvfv0bi  40566  fnbrafvb  40568  afvres  40586  tz6.12-afv  40587  afvco2  40590  ndmaovcl  40617  zm1nn  40643  nltle2tri  40650  subsubelfzo0  40663  iccpartres  40682  iccpartiltu  40686  fargshiftfv  40703  pfxfv  40728  pfxsuff1eqwrdeq  40736  reuccatpfxs1lem  40762  fmtnof1  40776  goldbachthlem2  40787  fmtnoprmfac1  40806  fmtnoprmfac2  40808  lighneallem2  40852  lighneallem4b  40855  lighneallem4  40856  evennodd  40885  oddneven  40886  oexpnegALTV  40917  oexpnegnz  40918  gboge7  40976  gbege6  40978  bgoldbwt  40990  bgoldbst  40991  nnsum3primesle9  41001  bgoldbtbndlem2  41013  prsprel  41055  sprsymrelf1lem  41059  sprsymrelfolem2  41061  sprsymrelfo  41065  mgmpropd  41093  clintop  41162  isassintop  41164  lidldomn1  41239  uzlidlring  41247  2zrngnmlid2  41269  rngccatidALTV  41307  ringccatidALTV  41370  srhmsubc  41394  srhmsubcALTV  41412  ztprmneprm  41443  pgrpgt2nabl  41465  lindslinindimp2lem4  41568  lincresunit3  41588  fldivexpfllog2  41681  digexp  41723  spd  41747  spcdvw  41748  setrec2fun  41762
  Copyright terms: Public domain W3C validator