Theorem biimpd 218

Description: Deduce an implication from a logical equivalence. Deduction associated with biimp 204 and biimpi 205. (Contributed by NM, 11-Jan-1993.)

Hypothesis

Ref	Expression
biimpd.1	⊢ (𝜑 → (𝜓 ↔ 𝜒))

Assertion

Ref	Expression
biimpd	⊢ (𝜑 → (𝜓 → 𝜒))

Proof of Theorem biimpd

Step	Hyp	Ref	Expression
1		biimpd.1	. 2 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
2		biimp 204	. 2 ⊢ ((𝜓 ↔ 𝜒) → (𝜓 → 𝜒))
3	1, 2	syl 17	1 ⊢ (𝜑 → (𝜓 → 𝜒))

Syntax hints:   → wi 4   ↔ wb 195

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 196

This theorem is referenced by:  mpbid  221  sylibd  228  sylbid  229  mpbidi  230  syl5ib  233  syl6bi  242  ibi  255  con4bid  306  mtbird  314  mtbiri  316  imbi1d  330  bitr3  341  pm5.21im  363  biimpa  500  alexbii  1750  exintr  1810  spfw  1952  spfwOLD  1953  cbvalw  1955  alcomiw  1958  stdpc5OLD  2064  cbvalv1  2163  spimt  2241  spv  2248  chvar  2250  cbval  2259  nfsb4t  2377  2eu3  2543  eqrdav  2609  rgen2a  2960  ralcom2  3083  raleleq  3133  ceqsalgALT  3204  vtoclf  3231  vtocl  3232  vtocl2  3234  vtocl3  3235  spcdv  3264  rspcdv  3285  rexraleqim  3299  elabgt  3316  sbcn1  3448  sbcim1  3449  sbcbi1  3450  sbeqalb  3455  sbcel21v  3464  eqrd  3586  elpwunsn  4171  rabsnifsb  4201  ssunsn2  4299  preqr1g  4325  propeqop  4895  euotd  4900  sotr2  4988  relop  5194  elres  5355  restidsingOLD  5378  elimasni  5411  sotri2  5444  relcnvtr  5572  onmindif  5732  iotaval  5779  dffv2  6181  mpteqb  6207  elfvmptrab  6214  chfnrn  6236  elpreima  6245  iinpreima  6253  exfo  6285  ffnfv  6295  f1elima  6421  f1eqcocnv  6456  fliftfun  6462  soisores  6477  isotr  6486  isomin  6487  ovmpt2dv2  6692  difsnexi  6864  onint  6887  oneqmin  6897  ordunisuc2  6936  tfindsg  6952  findsg  6985  f1oweALT  7043  el2mpt2cl  7138  ressuppss  7201  funsssuppss  7208  imacosupp  7222  smoiso  7346  seqomlem2  7433  oaordi  7513  oawordri  7517  oaordex  7525  oalimcl  7527  omwordi  7538  oewordi  7558  oelim2  7562  nnmwordi  7602  xpider  7705  iiner  7706  undifixp  7830  mptelixpg  7831  dom2lem  7881  nneneq  8028  fineqvlem  8059  pssnn  8063  dif1en  8078  findcard2s  8086  unfilem2  8110  xpfi  8116  domunfican  8118  f1dmvrnfibi  8133  fsuppimp  8164  dffi2  8212  wemaplem2  8335  suc11reg  8399  noinfep  8440  cantnflem1  8469  r1fin  8519  tcrank  8630  cardlim  8681  pr2nelem  8710  fseqenlem1  8730  alephnbtwn  8777  alephord2i  8783  alephf1  8791  cardaleph  8795  alephiso  8804  dfac12lem2  8849  ackbij1lem16  8940  cflm  8955  cfcoflem  8977  sornom  8982  fin23lem27  9033  isf32lem7  9064  fin17  9099  fin1a2lem2  9106  fin1a2lem4  9108  fin1a2lem6  9110  fin1a2lem9  9113  axdc3lem2  9156  zorn2lem7  9207  uniimadom  9245  inar1  9476  grothomex  9530  addcanpi  9600  mulcanpi  9601  enqer  9622  genpcd  9707  genpnmax  9708  ltexprlem4  9740  reclem3pr  9750  reclem4pr  9751  suplem2pr  9754  axpre-ltadd  9867  axpre-sup  9869  ltletr  10008  00id  10090  addn0nid  10330  mul0or  10546  prodgt02  10748  prodge02  10750  lemul1a  10756  mulgt1  10761  divgt0  10770  divge0  10771  ledivp1i  10828  ltdivp1i  10829  cju  10893  nnsub  10936  nominpos  11146  nn0n0n1ge2  11235  btwnnz  11329  suprfinzcl  11368  ublbneg  11649  zmax  11661  cnref1o  11703  ltsubrp  11742  ltaddrp  11743  xrltletr  11864  qbtwnre  11904  xltnegi  11921  xnn0xadd0  11949  iccsupr  12137  icoshft  12165  difreicc  12175  iccshftri  12178  iccshftli  12180  iccdili  12182  icccntri  12184  fzen  12229  fzofzim  12382  eluzgtdifelfzo  12397  elfzo1elm1fzo0  12435  injresinjlem  12450  injresinj  12451  flval2  12477  flval3  12478  modmuladdim  12575  modaddmodup  12595  addmodlteq  12607  fseqsupubi  12639  ssnn0fi  12646  mptnn0fsuppr  12661  sq01  12848  hashf1rn  13004  hashf1rnOLD  13005  hashgt12el  13070  hashgt12el2  13071  hash2pr  13108  hash2exprb  13110  hashge2el2difr  13118  hashtpg  13121  hash3tr  13127  lswlgt0cl  13209  ccatalpha  13228  2swrd1eqwrdeq  13306  ccatopth2  13323  reuccats1lem  13331  swrdccatin2  13338  swrdccat  13344  swrdccat3a  13345  swrdccat3blem  13346  repsdf2  13376  repswsymball  13377  repswrevw  13384  cshweqrep  13418  cshw1  13419  2cshwcshw  13422  scshwfzeqfzo  13423  cshwcsh2id  13425  swrdco  13434  swrd2lsw  13543  2swrd2eqwrdeq  13544  wwlktovfo  13549  cjre  13727  icodiamlt  14022  o1lo1  14116  o1of2  14191  o1rlimmul  14197  zsum  14296  modfsummods  14366  zprod  14506  reeff1  14689  dvds2lem  14832  muldvds1  14844  dvdscmulr  14848  dvdsmulcr  14849  dvdsdivcl  14876  mod2eq1n2dvds  14909  oddnn02np1  14910  divalglem8  14961  ndvdsadd  14972  zeqzmulgcd  15070  dfgcd2  15101  gcdmultiple  15107  absproddvds  15168  lcmftp  15187  coprmdvds  15204  isprm5  15257  divgcdodd  15260  isprm6  15264  prmdvdsexpr  15267  cncongrprm  15275  phiprmpw  15319  modprm0  15348  pythagtriplem4  15362  pcz  15423  difsqpwdvds  15429  1arith  15469  prmgaplem5  15597  prmgaplem6  15598  cshwrepswhash1  15647  divsfval  16030  catsubcat  16322  fthmon  16410  isinitoi  16476  istermoi  16477  iszeroi  16482  setcmon  16560  setcepi  16561  funcestrcsetclem8  16610  fthestrcsetc  16613  funcsetcestrclem8  16625  fthsetcestrc  16628  pltnle  16789  pltval3  16790  lublecllem  16811  latasym  16878  odupos  16958  mrelatglb  17007  mrelatlub  17009  cnvpsb  17036  isgrpid2  17281  ghmghmrn  17502  ghmf1  17512  orbsta  17569  resscntz  17587  gsmsymgrfixlem1  17670  gsmsymgreqlem2  17674  mndodcongi  17785  odf1  17802  lsmss1  17902  lsmss2  17904  efgredeu  17988  cntzcmnss  18069  lt6abl  18119  ablfaclem3  18309  ringinvnz1ne0  18415  kerf1hrm  18566  lspsneq  18943  lspsneu  18944  lsmcv  18962  lidldvgen  19076  0ringnnzr  19090  domnmuln0  19119  opprdomn  19122  ply1scln0  19482  gsummoncoe1  19495  domnchr  19699  znf1o  19719  zntoslem  19724  znfld  19728  cygznlem2a  19735  cygznlem3  19737  islindf4  19996  uvcendim  20005  matvscl  20056  scmataddcl  20141  scmatsubcl  20142  scmatfo  20155  scmatghm  20158  maducoeval2  20265  slesolinv  20305  cramerimplem2  20309  cpmatelimp  20336  cpmatelimp2  20338  cpmatacl  20340  cpmatinvcl  20341  pm2mpf1  20423  cayhamlem1  20490  cayleyhamilton1  20516  0ntr  20685  islpi  20763  lmss  20912  cmpcld  21015  cmpfi  21021  1stcelcls  21074  comppfsc  21145  ptcnplem  21234  qtophmeo  21430  fbdmn0  21448  fbasrn  21498  elfm3  21564  fmfnfmlem4  21571  fclscf  21639  cnpfcf  21655  alexsubALTlem3  21663  tsmsres  21757  blval2  22177  tnggrpr  22269  nmoleub  22345  nmhmcn  22728  ncvs1  22765  iscau4  22885  caussi  22903  cniccbdd  23037  ovoliunnul  23082  mbfinf  23238  itg2splitlem  23321  dvcn  23490  c1lip1  23564  c1lip3  23566  dvcnvrelem1  23584  ply1divex  23700  quotcan  23868  aannenlem1  23887  taylf  23919  ulmcaulem  23952  ulmcau  23953  reeff1o  24005  logccv  24209  logreclem  24300  isosctrlem2  24349  xrlimcnp  24495  rlimcxp  24500  ftalem7  24605  vmappw  24642  fsumvma  24738  dchreq  24783  dchrptlem1  24789  dchrsum  24794  bposlem7  24815  lgsqrlem2  24872  lgsdchr  24880  gausslemma2dlem1a  24890  lgseisenlem2  24901  lgsquad2  24911  2lgslem1b  24917  2sqlem6  24948  tgcgrcomimp  25172  isperp2  25410  xmstrkgc  25566  brbtwn  25579  brcgr  25580  axcgrid  25596  axeuclidlem  25642  axeuclid  25643  lpvtx  25734  upgrex  25759  upgredgpr  25815  uhgraeq12d  25836  usgrac  25880  usgraeq12d  25891  usgranloopv  25907  nbgraf1olem5  25974  iscusgra0  25986  cusgrasize2inds  26005  cusgrafilem3  26009  usgramaxsize  26015  iswlkg  26052  wlkcompim  26054  wlkcpr  26057  wlkonprop  26063  trlonprop  26072  0wlkon  26077  usgrwlknloop  26093  pthonprop  26107  spthonprp  26115  redwlk  26136  wlkdvspthlem  26137  usgra2wlkspthlem2  26148  fargshiftfv  26163  wwlknimp  26215  vfwlkniswwlkn  26234  usg2wlkeq  26236  wwlknred  26251  wwlknext  26252  wwlknextbi  26253  wwlkextwrd  26256  wwlkextinj  26258  wwlkextsur  26259  wwlkm1edg  26263  isclwlkg  26283  clwlkcompim  26292  0clwlk  26293  clwwlkn2  26303  clwlkisclwwlklem2a1  26307  clwlkisclwwlklem2a4  26312  clwlkisclwwlklem2a  26313  clwlkisclwwlklem1  26315  clwwlkf  26322  wwlkext2clwwlk  26331  clwwisshclwwlem1  26333  wlklenvclwlk  26366  clwlkfclwwlk  26371  el2spthonot  26397  usg2wotspth  26411  usg2spthonot  26415  usg2spthonot0  26416  rgraprop  26455  rusgraprop  26456  rusgraprop3  26470  frgranbnb  26547  frgrancvvdeqlem3  26559  frgrancvvdeqlem4  26560  frgrancvvdeqlem7  26563  frgrawopreglem2  26572  frgrawopreg  26576  frgregordn0  26597  clwwlkextfrlem1  26603  extwwlkfablem2  26605  numclwwlkovf2ex  26613  numclwlk1lem2foa  26618  numclwlk1lem2f1  26621  numclwwlk8  26642  hlipgt0  27154  ocin  27539  ocnel  27541  shmodsi  27632  pjmf1  27959  unopf1o  28159  staddi  28489  stadd3i  28491  mdi  28538  dmdmd  28543  dmdi  28545  dmdbr2  28546  dmdbr3  28548  dmdbr4  28549  dmdi4  28550  mdsl1i  28564  superpos  28597  cvbr4i  28610  atssma  28621  atcv1  28623  atomli  28625  chirredlem1  28633  addltmulALT  28689  bian1d  28690  ifeqeqx  28745  disjxpin  28783  suppss3  28890  fpwrelmap  28896  ogrpaddlt  29049  metider  29265  tpr2rico  29286  xrge0iifiso  29309  qqhcn  29363  qqhucn  29364  esumlub  29449  esumpinfval  29462  esumpinfsum  29466  ballotlemfc0  29881  ballotlemfcc  29882  bnj517  30209  erdsze2lem2  30440  trpredrec  30982  poseq  30994  soseq  30995  sltval2  31053  sltres  31061  nodenselem7  31086  nodenselem8  31087  nodense  31088  nobndup  31099  nobnddown  31100  nofulllem5  31105  dfrdg4  31228  altopthsn  31238  btwncomim  31290  btwnexch3  31297  btwnexch2  31300  endofsegid  31362  opnrebl2  31486  nn0prpwlem  31487  onsuct0  31610  ordcmp  31616  nndivsub  31626  dnibndlem13  31650  bj-cbvexw  31851  bj-cbv3tb  31898  bj-spimtv  31905  bj-spvv  31910  bj-chvarv  31912  bj-equsal  32001  bj-sbsb  32012  bj-ax8  32080  bj-vtoclf  32100  bj-snsetex  32144  bj-inftyexpiinj  32273  bj-finsumval0  32324  bj-bary1lem1  32338  bj-bary1  32339  f1omptsnlem  32359  iooelexlt  32386  relowlpssretop  32388  rdgeqoa  32394  finxpsuclem  32410  wl-equsal1i  32508  wl-ax11-lem10  32550  ltflcei  32567  sin2h  32569  cos2h  32570  tan2h  32571  lindsenlbs  32574  matunitlindf  32577  poimirlem3  32582  poimirlem4  32583  poimirlem18  32597  poimirlem20  32599  poimirlem21  32600  poimirlem22  32601  poimirlem24  32603  poimirlem25  32604  poimirlem26  32605  poimirlem27  32606  poimirlem28  32607  poimirlem31  32610  poimir  32612  heicant  32614  mblfinlem1  32616  mblfinlem2  32617  mblfinlem3  32618  mblfinlem4  32619  mbfresfi  32626  cnambfre  32628  ftc1anc  32663  dvasin  32666  areacirclem1  32670  areacirclem4  32673  areacirc  32675  brabg2  32680  fzmul  32707  fdc  32711  incsequz2  32715  isbnd2  32752  opidonOLD  32821  opidon2OLD  32823  grpomndo  32844  elghomlem2OLD  32855  rngoueqz  32909  dvrunz  32923  divrngidl  32997  dral1-o  33207  lsatn0  33304  l1cvpat  33359  leat2  33599  atnle  33622  cvlcvr1  33644  cvrexchlem  33723  cvratlem  33725  cvrat  33726  atcvrj0  33732  atle  33740  snatpsubN  34054  linepsubN  34056  pmapsub  34072  lneq2at  34082  lncvrelatN  34085  2llnma3r  34092  cdlemblem  34097  paddasslem5  34128  poml4N  34257  lhpmcvr4N  34330  trlval2  34468  cdlemd6  34508  cdleme7ga  34553  cdleme25b  34660  cdleme29b  34681  cdleme35fnpq  34755  cdleme50f1  34849  cdlemf1  34867  cdlemg27b  35002  cdlemk28-3  35214  tendospcanN  35330  diaf11N  35356  dia2dimlem1  35371  dibf11N  35468  dihf11  35574  dihmeetlem1N  35597  dochvalr  35664  dochnel2  35699  dvh4dimlem  35750  dochsat0  35764  mapd1o  35955  hdmapf1oN  36175  hgmapval0  36202  hgmapf1oN  36213  hlhilhillem  36270  rexrabdioph  36376  fphpdo  36399  irrapxlem3  36406  rmxypairf1o  36494  rmxycomplete  36500  zindbi  36529  lermxnn0  36535  ltrmy  36537  rmyeq0  36538  rmyeq  36539  lermy  36540  acongsym  36561  acongneg2  36562  wepwsolem  36630  intabssd  36935  ss2iundf  36970  frege129d  37074  frege133d  37076  axfrege52a  37170  axfrege52c  37201  ntrk0kbimka  37357  gneispace  37452  suprleubrd  37488  suprlubrd  37492  radcnvrat  37535  nzss  37538  expgrowthi  37554  ordpss  37676  bi23impib  37712  bi23imp13  37718  rspsbc2  37765  tratrb  37767  sbcim2g  37769  truniALT  37772  3impcombi  38065  tpid3gVD  38099  orbi1rVD  38105  sbc3orgVD  38108  rspsbc2VD  38112  tratrbVD  38119  sbcim2gVD  38133  sbcbiVD  38134  truniALTVD  38136  trintALTVD  38138  trintALT  38139  csbingVD  38142  csbsngVD  38151  csbxpgVD  38152  csbresgVD  38153  csbrngVD  38154  csbima12gALTVD  38155  csbunigVD  38156  csbfv12gALTVD  38157  relopabVD  38159  isosctrlem1ALT  38192  fzisoeu  38455  xrralrecnnge  38554  allbutfi  38557  climinf  38673  stoweidlem7  38900  stoweidlem62  38955  sge0gerpmpt  39295  meaiuninclem  39373  carageniuncllem2  39412  issmflem  39613  2reu3  39837  ralbinrald  39848  funressnfv  39857  afv0fv0  39878  afv0nbfvbi  39880  afvfv0bi  39881  fnbrafvb  39883  afvres  39901  tz6.12-afv  39902  afvco2  39905  ndmaovcl  39932  nltle2tri  39942  iccpartres  39956  iccpartiltu  39960  fmtnof1  39985  goldbachthlem2  39996  fmtnoprmfac1  40015  fmtnoprmfac2  40017  lighneallem2  40061  lighneallem4b  40064  lighneallem4  40065  evennodd  40094  oddneven  40095  oexpnegALTV  40126  oexpnegnz  40127  gboge7  40185  gbege6  40187  bgoldbwt  40199  bgoldbst  40200  nnsum3primesle9  40210  bgoldbtbndlem2  40222  pfxfv  40262  pfxsuff1eqwrdeq  40270  reuccatpfxs1lem  40296  zm1nn  40348  subsubelfzo0  40359  uhgr0v0e  40464  subgrprop  40497  fusgrfisbase  40547  edgnbusgreu  40595  nbusgredgeu0  40596  cusgredg  40646  cusgrsize2inds  40669  cusgrsize  40670  usgredgsscusgredg  40675  fusgrmaxsize  40680  uspgrloopvtxel  40732  umgr2v2e  40741  rgrprop  40760  rusgrprop  40762  0uhgrrusgr  40778  rusgrpropedg  40784  ewlkprop  40805  upgrewlkle2  40808  upgr1wlkcompim  40851  uspgr2wlkeq  40854  1wlklenvclwlk  40863  wlkOnprop  40866  1wlkres  40879  red1wlk  40881  1wlkdlem2  40892  1wlksonproplem  40912  usgr2trlspth  40967  usgr2pth  40970  pthdlem1  40972  isclWlkb  40980  crctprop  40998  cyclprop  40999  crctcsh1wlkn0lem4  41016  wspthnonp  41055  1wlkiswwlks2  41072  wwlksm1edg  41078  wlknewwlksn  41084  wwlksnred  41098  wwlksnext  41099  wwlksnextbi  41100  wwlksnextwrd  41103  wwlksnextinj  41105  wwlksnextsur  41106  umgr2wlk  41156  umgrwwlks2on  41161  elwspths2on  41163  usgr2wspthons3  41167  elwwlks2  41170  clwwlknp  41195  clwlkclwwlklem2a1  41201  clwlkclwwlklem2a4  41206  clwlkclwwlklem2a  41207  clwlkclwwlklem2  41209  clwwlks1loop  41215  umgrclwwlksge2  41219  clwwlksf  41222  wwlksext2clwwlk  41231  clwwisshclwwslemlem  41233  clwwnisshclwwsn  41237  clwlksfclwwlk  41269  vdn0conngrumgrv2  41363  eupthtrli  41370  eupthi  41371  upgreupthi  41376  frgrnbnb  41463  frgrncvvdeqlem3  41471  frgrncvvdeqlem4  41472  frgrncvvdeqlem7  41475  frgrwopreg  41486  fusgr2wsp2nb  41498  frrusgrord0  41503  av-clwwlkextfrlem1  41509  av-numclwwlkovf2ex  41517  av-numclwlk1lem2foa  41521  av-numclwwlk8  41546  av-frgrareg  41548  mgmpropd  41565  clintop  41634  isassintop  41636  lidldomn1  41711  uzlidlring  41719  2zrngnmlid2  41741  rngccatidALTV  41781  ringccatidALTV  41844  srhmsubc  41868  srhmsubcALTV  41887  ztprmneprm  41918  pgrpgt2nabl  41941  lindslinindimp2lem4  42044  lincresunit3  42064  fldivexpfllog2  42157  digexp  42199  spd  42223  spcdvw  42224  setrec2fun  42238