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  502  alexbii  1905  exintr  1964  spfw  2112  spfwOLD  2113  cbvalw  2115  alcomiw  2118  stdpc5OLD  2220  cbvalv1  2316  spimt  2394  spv  2401  chvar  2403  cbval  2412  nfsb4t  2522  2eu3  2689  eqrdav  2755  rgen2a  3111  ralcom2  3238  raleleq  3291  ceqsalgALT  3367  vtoclf  3394  vtocl  3395  vtocl2  3397  vtocl3  3398  spcdv  3427  rspcdv  3448  rspcebdv  3450  rexraleqim  3463  elabgt  3483  sbcn1  3618  sbcim1  3619  sbcbi1  3620  sbeqalb  3625  sbcel21v  3634  eqrdOLD  3760  elpwunsn  4364  rabsnifsb  4397  ssunsn2  4500  preqr1g  4525  propeqop  5114  euotd  5119  sotr2  5212  relop  5424  elres  5589  restidsingOLD  5613  elimasni  5646  sotri2  5679  relcnvtr  5812  onmindif  5972  iotaval  6019  dffv2  6429  mpteqb  6457  elfvmptrab  6464  chfnrn  6487  elpreima  6496  iinpreima  6504  exfo  6536  ffnfv  6547  f1elima  6679  f1eqcocnv  6715  fliftfun  6721  soisores  6736  isotr  6745  isomin  6746  ovmpt2dv2  6955  difsnexi  7131  onint  7156  oneqmin  7166  ordunisuc2  7205  tfindsg  7221  findsg  7254  f1oweALT  7313  el2mpt2cl  7415  ressuppss  7478  funsssuppss  7486  imacosupp  7500  smoiso  7624  seqomlem2  7711  oaordi  7791  oawordri  7795  oaordex  7803  oalimcl  7805  omwordi  7816  oewordi  7836  oelim2  7840  nnmwordi  7880  xpider  7981  iiner  7982  undifixp  8106  mptelixpg  8107  dom2lem  8157  nneneq  8304  fineqvlem  8335  pssnn  8339  dif1en  8354  findcard2s  8362  unfilem2  8386  xpfi  8392  domunfican  8394  f1dmvrnfibi  8411  fsuppimp  8442  dffi2  8490  wemaplem2  8613  suc11reg  8685  noinfep  8726  cantnflem1  8755  r1fin  8805  tcrank  8916  cardlim  8984  pr2nelem  9013  fseqenlem1  9033  alephnbtwn  9080  alephord2i  9086  alephf1  9094  cardaleph  9098  alephiso  9107  dfac12lem2  9154  ackbij1lem16  9245  cflm  9260  cfcoflem  9282  sornom  9287  fin23lem27  9338  isf32lem7  9369  fin17  9404  fin1a2lem2  9411  fin1a2lem4  9413  fin1a2lem6  9415  fin1a2lem9  9418  axdc3lem2  9461  zorn2lem7  9512  uniimadom  9554  inar1  9785  grothomex  9839  addcanpi  9909  mulcanpi  9910  enqer  9931  genpcd  10016  genpnmax  10017  ltexprlem4  10049  reclem3pr  10059  reclem4pr  10060  suplem2pr  10063  axpre-ltadd  10176  axpre-sup  10178  ltletr  10317  00id  10399  addn0nid  10639  mul0or  10855  prodgt02  11057  prodge02  11059  lemul1a  11065  mulgt1  11070  divgt0  11079  divge0  11080  ledivp1i  11137  ltdivp1i  11138  cju  11204  nnsub  11247  nominpos  11457  nn0n0n1ge2  11546  btwnnz  11641  suprfinzcl  11680  ublbneg  11962  zmax  11974  cnref1o  12016  ltsubrp  12055  ltaddrp  12056  xrltletr  12177  qbtwnre  12219  xltnegi  12236  xnn0xadd0  12266  iccsupr  12455  icoshft  12483  difreicc  12493  iccshftri  12496  iccshftli  12498  iccdili  12500  icccntri  12502  fzen  12547  elfz1b  12598  fzofzim  12705  eluzgtdifelfzo  12720  elfzo1elm1fzo0  12759  injresinjlem  12778  injresinj  12779  flval2  12805  flval3  12806  modmuladdim  12903  modaddmodup  12923  addmodlteq  12935  fseqsupubi  12967  ssnn0fi  12974  mptnn0fsuppr  12989  sq01  13176  hashf1rn  13331  hashgt12el  13398  hashgt12el2  13399  hash2pr  13439  hash2exprb  13441  hashge2el2difr  13451  hashtpg  13455  hash3tr  13460  lswlgt0cl  13539  ccatalpha  13561  2swrd1eqwrdeq  13650  ccatopth2  13667  reuccats1lem  13675  swrdccatin2  13683  swrdccat  13689  swrdccat3a  13690  swrdccat3blem  13691  repsdf2  13721  repswsymball  13722  repswrevw  13729  cshweqrep  13763  cshw1  13764  2cshwcshw  13767  scshwfzeqfzo  13768  cshwcsh2id  13770  swrdco  13779  swrd2lsw  13892  2swrd2eqwrdeq  13893  wwlktovfo  13898  cjre  14074  icodiamlt  14369  o1lo1  14463  o1of2  14538  o1rlimmul  14544  zsum  14644  modfsummods  14720  zprod  14862  reeff1  15045  dvdsmod0  15184  dvds2lem  15192  muldvds1  15204  dvdscmulr  15208  dvdsmulcr  15209  dvdsdivcl  15236  mod2eq1n2dvds  15269  oddnn02np1  15270  divalglem8  15321  ndvdsadd  15332  zeqzmulgcd  15430  dfgcd2  15461  gcdmultiple  15467  absproddvds  15528  lcmftp  15547  coprmdvds  15564  isprm5  15617  divgcdodd  15620  isprm6  15624  prmdvdsexpr  15627  cncongrprm  15635  phiprmpw  15679  modprm0  15708  pythagtriplem4  15722  pcz  15783  difsqpwdvds  15789  1arith  15829  prmgaplem5  15957  prmgaplem6  15958  cshwrepswhash1  16007  divsfval  16405  catsubcat  16696  fthmon  16784  isinitoi  16850  istermoi  16851  iszeroi  16856  setcmon  16934  setcepi  16935  funcestrcsetclem8  16984  fthestrcsetc  16987  funcsetcestrclem8  16999  fthsetcestrc  17002  pltnle  17163  pltval3  17164  lublecllem  17185  latasym  17252  odupos  17332  mrelatglb  17381  mrelatlub  17383  cnvpsb  17410  isgrpid2  17655  ghmghmrn  17876  ghmf1  17886  orbsta  17942  resscntz  17960  gsmsymgrfixlem1  18043  gsmsymgreqlem2  18047  mndodcongi  18158  odf1  18175  lsmss1  18275  lsmss2  18277  efgredeu  18361  cntzcmnss  18442  lt6abl  18492  ablfaclem3  18682  ringinvnz1ne0  18788  kerf1hrm  18941  lspsneq  19320  lspsneu  19321  lsmcv  19339  lidldvgen  19453  0ringnnzr  19467  domnmuln0  19496  opprdomn  19499  ply1scln0  19859  gsummoncoe1  19872  domnchr  20078  znf1o  20098  zntoslem  20103  znfld  20107  cygznlem2a  20114  cygznlem3  20116  islindf4  20375  uvcendim  20384  matvscl  20435  scmataddcl  20520  scmatsubcl  20521  scmatfo  20534  scmatghm  20537  maducoeval2  20644  slesolinv  20684  cramerimplem2  20688  cpmatelimp  20715  cpmatelimp2  20717  cpmatacl  20719  cpmatinvcl  20720  pm2mpf1  20802  cayhamlem1  20869  cayleyhamilton1  20895  0ntr  21073  islpi  21151  lmss  21300  cmpcld  21403  cmpfi  21409  1stcelcls  21462  comppfsc  21533  ptcnplem  21622  qtophmeo  21818  fbdmn0  21835  fbasrn  21885  elfm3  21951  fmfnfmlem4  21958  fclscf  22026  cnpfcf  22042  alexsubALTlem3  22050  tsmsres  22144  blval2  22564  tnggrpr  22656  nmoleub  22732  nmhmcn  23116  ncvs1  23153  iscau4  23273  caussi  23291  cniccbdd  23426  ovoliunnul  23471  mbfinf  23627  itg2splitlem  23710  dvcn  23879  c1lip1  23955  c1lip3  23957  dvcnvrelem1  23975  ply1divex  24091  quotcan  24259  aannenlem1  24278  taylf  24310  ulmcaulem  24343  ulmcau  24344  reeff1o  24396  logccv  24604  logreclem  24695  isosctrlem2  24744  xrlimcnp  24890  rlimcxp  24895  ftalem7  25000  vmappw  25037  fsumvma  25133  dchreq  25178  dchrptlem1  25184  dchrsum  25189  bposlem7  25210  lgsqrlem2  25267  lgsdchr  25275  gausslemma2dlem1a  25285  lgseisenlem2  25296  lgsquad2  25306  2lgslem1b  25312  2sqlem6  25343  tgcgrcomimp  25567  isperp2  25805  xmstrkgc  25961  brbtwn  25974  brcgr  25975  axcgrid  25991  axeuclidlem  26037  axeuclid  26038  lpvtx  26158  upgrex  26182  upgrpredgv  26229  upgredgpr  26232  uhgr0v0e  26325  subgrprop  26360  fusgrfisbase  26415  edgnbusgreu  26463  nbusgredgeu0  26464  cusgredg  26526  structtocusgr  26548  cusgrsize2inds  26555  cusgrsize  26556  usgredgsscusgredg  26561  fusgrmaxsize  26566  uspgrloopvtxel  26618  umgr2v2e  26627  vtxdginducedm1fi  26646  finsumvtxdg2sstep  26651  rgrprop  26662  rusgrprop  26664  0uhgrrusgr  26680  rusgrpropedg  26686  ewlkprop  26705  upgrewlkle2  26708  wlkprop  26713  upgrwlkcompim  26745  uspgr2wlkeq  26748  wlklenvclwlk  26757  wlkonprop  26760  wlkres  26773  redwlk  26775  wlkdlem2  26786  wksonproplem  26807  usgr2trlspth  26863  usgr2pth  26866  pthdlem1  26868  crctcshwlkn0lem4  26912  wwlksnprcl  26938  wlkiswwlks2  26980  wwlksm1edg  26986  wlknewwlksn  26992  wwlksnred  27006  wwlksnext  27007  wwlksnextbi  27008  wwlksnextwrd  27011  wwlksnextinj  27013  wwlksnextsur  27014  umgr2wlk  27065  umgrwwlks2on  27074  elwwlks2  27084  clwwlk1loop  27107  clwwlkccatlem  27108  umgrclwwlkge2  27110  clwlkclwwlklem2a1  27111  clwlkclwwlklem2a4  27116  clwlkclwwlklem2a  27117  clwlkclwwlklem2  27119  clwlkclwwlkfo  27128  clwwisshclwwslemlem  27132  clwwlknwwlksn  27162  clwwlknwwlksnOLD  27163  clwwlknlbonbgr1  27164  clwwlkn1loopb  27168  clwwlkf  27172  wwlksext2clwwlk  27183  wwlksext2clwwlkOLD  27184  clwlksfclwwlkOLD  27212  clwwlknon1  27241  clwwlknonwwlknonb  27250  clwwlknonwwlknonbOLD  27251  clwwlknonex2lem2  27253  vdn0conngrumgrv2  27344  frgrnbnb  27443  frgrncvvdeqlem2  27450  frgrncvvdeqlem3  27451  frgrncvvdeqlem6  27454  frgrwopreglem4a  27460  fusgr2wsp2nb  27484  frrusgrord0lem  27489  numclwwlk2lem1lem  27494  numclwwlk2lem1lemOLD  27495  2clwwlk2clwwlklem  27499  2clwwlk2clwwlk  27503  numclwlk1lem2foa  27509  numclwlk1lem2f1  27512  frgrreg  27558  hlipgt0  28075  ocin  28460  ocnel  28462  shmodsi  28553  pjmf1  28880  unopf1o  29080  staddi  29410  stadd3i  29412  mdi  29459  dmdmd  29464  dmdi  29466  dmdbr2  29467  dmdbr3  29469  dmdbr4  29470  dmdi4  29471  mdsl1i  29485  superpos  29518  cvbr4i  29531  atssma  29542  atcv1  29544  atomli  29546  chirredlem1  29554  addltmulALT  29610  bian1d  29611  ifeqeqx  29664  disjxpin  29704  suppss3  29807  fpwrelmap  29813  ogrpaddlt  30023  metider  30242  tpr2rico  30263  xrge0iifiso  30286  qqhcn  30340  qqhucn  30341  esumlub  30427  esumpinfval  30440  esumpinfsum  30444  ballotlemfc0  30859  ballotlemfcc  30860  ftc2re  30981  bnj517  31258  erdsze2lem2  31489  trpredrec  32039  poseq  32055  soseq  32056  sltval2  32111  sltres  32117  nodenselem8  32143  nodense  32144  noresle  32148  scutun12  32219  madeval2  32238  dfrdg4  32360  altopthsn  32370  btwncomim  32422  btwnexch3  32429  btwnexch2  32432  endofsegid  32494  opnrebl2  32618  nn0prpwlem  32619  onsuct0  32742  ordcmp  32748  nndivsub  32758  dnibndlem13  32782  bj-cbvexw  32966  bj-cbv3tb  33013  bj-spimtv  33020  bj-spvv  33025  bj-chvarv  33027  bj-equsal  33115  bj-sbsb  33126  bj-ax8  33189  bj-vtoclf  33210  bj-snsetex  33253  bj-ismooredr2  33367  bj-inftyexpiinj  33403  bj-finsumval0  33454  bj-bary1lem1  33468  bj-bary1  33469  f1omptsnlem  33490  iooelexlt  33517  relowlpssretop  33519  rdgeqoa  33525  finxpsuclem  33541  wl-equsal1i  33638  wl-ax11-lem10  33680  ltflcei  33706  sin2h  33708  cos2h  33709  tan2h  33710  lindsenlbs  33713  matunitlindf  33716  poimirlem3  33721  poimirlem4  33722  poimirlem18  33736  poimirlem20  33738  poimirlem21  33739  poimirlem22  33740  poimirlem24  33742  poimirlem25  33743  poimirlem26  33744  poimirlem27  33745  poimirlem28  33746  poimirlem31  33749  poimir  33751  heicant  33753  mblfinlem1  33755  mblfinlem2  33756  mblfinlem3  33757  mblfinlem4  33758  mbfresfi  33765  cnambfre  33767  ftc1anc  33802  dvasin  33805  areacirclem1  33809  areacirclem4  33812  areacirc  33814  brabg2  33819  fzmul  33846  fdc  33850  incsequz2  33854  isbnd2  33891  opidonOLD  33960  opidon2OLD  33962  grpomndo  33983  elghomlem2OLD  33994  rngoueqz  34048  dvrunz  34062  divrngidl  34136  dral1-o  34689  lsatn0  34785  l1cvpat  34840  leat2  35080  atnle  35103  cvlcvr1  35125  cvrexchlem  35204  cvratlem  35206  cvrat  35207  atcvrj0  35213  atle  35221  snatpsubN  35535  linepsubN  35537  pmapsub  35553  lneq2at  35563  lncvrelatN  35566  2llnma3r  35573  cdlemblem  35578  paddasslem5  35609  poml4N  35738  lhpmcvr4N  35811  trlval2  35949  cdlemd6  35989  cdleme7ga  36034  cdleme25b  36140  cdleme29b  36161  cdleme35fnpq  36235  cdleme50f1  36329  cdlemf1  36347  cdlemg27b  36482  cdlemk28-3  36694  tendospcanN  36810  diaf11N  36836  dia2dimlem1  36851  dibf11N  36948  dihf11  37054  dihmeetlem1N  37077  dochvalr  37144  dochnel2  37179  dvh4dimlem  37230  dochsat0  37244  mapd1o  37435  hdmapf1oN  37655  hgmapval0  37682  hgmapf1oN  37693  hlhilhillem  37750  rexrabdioph  37856  fphpdo  37879  irrapxlem3  37886  rmxypairf1o  37974  rmxycomplete  37980  zindbi  38009  lermxnn0  38015  ltrmy  38017  rmyeq0  38018  rmyeq  38019  lermy  38020  acongsym  38041  acongneg2  38042  wepwsolem  38110  intabssd  38414  ss2iundf  38449  frege129d  38553  frege133d  38555  axfrege52a  38648  axfrege52c  38679  ntrk0kbimka  38835  gneispace  38930  suprleubrd  38964  suprlubrd  38968  radcnvrat  39011  nzss  39014  expgrowthi  39030  ordpss  39153  bi23impib  39189  bi23imp13  39195  rspsbc2  39242  tratrb  39244  sbcim2g  39246  truniALT  39249  3impcombi  39542  tpid3gVD  39572  orbi1rVD  39578  sbc3orgVD  39581  rspsbc2VD  39585  tratrbVD  39592  sbcim2gVD  39606  sbcbiVD  39607  truniALTVD  39609  trintALTVD  39611  trintALT  39612  csbingVD  39615  csbsngVD  39624  csbxpgVD  39625  csbresgVD  39626  csbrngVD  39627  csbima12gALTVD  39628  csbunigVD  39629  csbfv12gALTVD  39630  relopabVD  39632  isosctrlem1ALT  39665  fzisoeu  40009  xrralrecnnge  40107  allbutfi  40110  climinf  40337  liminfreuzlem  40533  climliminf  40537  climliminflimsup  40539  xlimbr  40552  stoweidlem7  40723  stoweidlem62  40778  sge0gerpmpt  41118  meaiuninclem  41196  carageniuncllem2  41238  issmflem  41438  2reu3  41690  ralbinrald  41701  funressnfv  41710  afv0fv0  41731  afv0nbfvbi  41733  afvfv0bi  41734  fnbrafvb  41736  afvres  41754  tz6.12-afv  41755  afvco2  41758  ndmaovcl  41785  nelbrim  41797  zm1nn  41822  nltle2tri  41829  subsubelfzo0  41842  iccpartres  41860  iccpartiltu  41864  fargshiftfv  41881  pfxfv  41905  pfxsuff1eqwrdeq  41913  reuccatpfxs1lem  41939  fmtnof1  41953  goldbachthlem2  41964  fmtnoprmfac1  41983  fmtnoprmfac2  41985  lighneallem2  42029  lighneallem4b  42032  lighneallem4  42033  evennodd  42062  oddneven  42063  oexpnegALTV  42094  oexpnegnz  42095  evenltle  42132  gbowge7  42157  gbege6  42159  sbgoldbwt  42171  sbgoldbst  42172  nnsum3primesle9  42188  bgoldbtbndlem2  42200  prsprel  42243  sprsymrelf1lem  42247  sprsymrelfolem2  42249  sprsymrelfo  42253  mgmpropd  42281  clintop  42350  isassintop  42352  lidldomn1  42427  uzlidlring  42435  2zrngnmlid2  42457  rngccatidALTV  42495  ringccatidALTV  42558  srhmsubc  42582  srhmsubcALTV  42600  ztprmneprm  42631  pgrpgt2nabl  42653  lindslinindimp2lem4  42756  lincresunit3  42776  fldivexpfllog2  42865  digexp  42907  spd  42931  spcdvw  42932  setrec2fun  42945
 Copyright terms: Public domain W3C validator