Theorem biimpd 220

Description: Deduce an implication from a logical equivalence. Deduction associated with biimp 206 and biimpi 207. (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 206	. 2 ⊢ ((𝜓 ↔ 𝜒) → (𝜓 → 𝜒))
3	1, 2	syl 17	1 ⊢ (𝜑 → (𝜓 → 𝜒))

Syntax hints:   → wi 4   ↔ wb 197

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 198

This theorem is referenced by:  mpbid  223  sylibd  230  sylbid  231  mpbidi  232  syl5ib  235  syl6bi  244  ibi  258  con4bid  308  mtbird  316  mtbiri  318  imbi1d  332  bitr3  343  pm5.21im  365  biimpa  464  alexbii  1917  exintr  1981  spfw  2131  spfwOLD  2132  cbvalw  2134  alcomiw  2137  alcomiwOLD  2138  stdpc5OLD  2243  cbvalv1  2347  spimt  2426  spv  2433  chvar  2435  cbval  2443  nfsb4t  2547  2eu3  2716  eqrdav  2801  rgen2a  3161  ralcom2  3288  raleleq  3341  ceqsalgALT  3421  vtoclf  3447  vtocl  3448  vtocl2  3450  vtocl3  3451  spcdv  3480  rspcdv  3501  rspcebdv  3503  rexraleqim  3518  elabgt  3538  sbcn1  3673  sbcim1  3674  sbcbi1  3675  sbeqalb  3680  sbcel21v  3688  eqrdOLD  3812  elpwunsn  4411  rabsnifsb  4442  ssunsn2  4542  preqr1g  4565  propeqop  5156  euotd  5162  sotr2  5255  relop  5468  elinxp  5631  elresOLD  5633  elimasni  5696  sotri2  5730  relcnvtr  5863  onmindif  6022  iotaval  6069  dffv2  6486  mpteqb  6514  elfvmptrab  6521  chfnrn  6544  elpreima  6553  iinpreima  6561  exfo  6593  ffnfv  6604  f1elima  6738  f1eqcocnv  6774  fliftfun  6780  soisores  6795  isotr  6804  isomin  6805  ovmpt2dv2  7018  difsnexi  7194  onint  7219  oneqmin  7229  ordunisuc2  7268  tfindsg  7284  findsg  7317  f1oweALT  7376  el2mpt2cl  7478  ressuppss  7542  funsssuppss  7550  imacosupp  7564  smoiso  7689  seqomlem2  7776  oaordi  7857  oawordri  7861  oaordex  7869  oalimcl  7871  omwordi  7882  oewordi  7902  oelim2  7906  nnmwordi  7946  xpider  8047  iiner  8048  undifixp  8175  mptelixpg  8176  dom2lem  8226  nneneq  8376  fineqvlem  8407  pssnn  8411  dif1en  8426  findcard2s  8434  unfilem2  8458  xpfi  8464  domunfican  8466  f1dmvrnfibi  8483  fsuppimp  8514  dffi2  8562  wemaplem2  8685  suc11reg  8757  noinfep  8798  cantnflem1  8827  r1fin  8877  tcrank  8988  cardlim  9075  pr2nelem  9104  fseqenlem1  9124  alephnbtwn  9171  alephord2i  9177  alephf1  9185  cardaleph  9189  alephiso  9198  dfac12lem2  9245  ackbij1lem16  9336  cflm  9351  cfcoflem  9373  sornom  9378  fin23lem27  9429  isf32lem7  9460  fin17  9495  fin1a2lem2  9502  fin1a2lem4  9504  fin1a2lem6  9506  fin1a2lem9  9509  axdc3lem2  9552  zorn2lem7  9603  uniimadom  9645  inar1  9876  grothomex  9930  addcanpi  10000  mulcanpi  10001  enqer  10022  genpcd  10107  genpnmax  10108  ltexprlem4  10140  reclem3pr  10150  reclem4pr  10151  suplem2pr  10154  axpre-ltadd  10267  axpre-sup  10269  ltletr  10408  00id  10490  addn0nid  10730  mul0or  10946  prodgt02  11148  prodge02OLD  11150  lemul1a  11156  mulgt1  11161  divgt0  11170  divge0  11171  ledivp1i  11228  ltdivp1i  11229  cju  11295  nnsub  11339  nominpos  11530  nn0n0n1ge2  11618  btwnnz  11713  suprfinzcl  11752  ublbneg  11986  zmax  11998  cnref1o  12035  ltsubrp  12074  ltaddrp  12075  xrltletr  12200  qbtwnre  12242  xltnegi  12259  xnn0xadd0  12289  iccsupr  12479  icoshft  12509  difreicc  12521  iccshftri  12524  iccshftli  12526  iccdili  12528  icccntri  12530  fzen  12575  elfz1b  12626  fzofzim  12733  eluzgtdifelfzo  12748  elfzo1elm1fzo0  12787  injresinjlem  12806  injresinj  12807  flval2  12833  flval3  12834  modmuladdim  12931  modaddmodup  12951  addmodlteq  12963  fseqsupubi  12995  ssnn0fi  13002  mptnn0fsuppr  13016  sq01  13203  hashf1rn  13355  hashgt12el  13421  hashgt12el2  13422  hash2pr  13462  hash2exprb  13464  hashge2el2difr  13474  hashtpg  13478  hash3tr  13483  lswlgt0cl  13562  ccatalpha  13584  2swrd1eqwrdeq  13672  ccatopth2  13689  reuccats1lem  13697  swrdccatin2  13705  swrdccat  13711  swrdccat3a  13712  swrdccat3blem  13713  repsdf2  13743  repswsymball  13744  repswrevw  13751  cshweqrep  13785  cshw1  13786  2cshwcshw  13789  scshwfzeqfzo  13790  cshwcsh2id  13792  swrdco  13801  swrd2lsw  13914  2swrd2eqwrdeq  13915  wwlktovfo  13920  cjre  14096  icodiamlt  14391  o1lo1  14485  o1of2  14560  o1rlimmul  14566  zsum  14666  modfsummods  14741  zprod  14882  reeff1  15064  dvdsmod0  15203  dvds2lem  15211  muldvds1  15223  dvdscmulr  15227  dvdsmulcr  15228  dvdsdivcl  15255  mod2eq1n2dvds  15285  oddnn02np1  15286  divalglem8  15337  ndvdsadd  15347  zeqzmulgcd  15445  dfgcd2  15476  gcdmultiple  15482  absproddvds  15543  lcmftp  15562  coprmdvds  15579  isprm5  15630  divgcdodd  15633  isprm6  15637  prmdvdsexpr  15640  cncongrprm  15648  phiprmpw  15692  modprm0  15721  pythagtriplem4  15735  pcz  15796  difsqpwdvds  15802  1arith  15842  prmgaplem5  15970  prmgaplem6  15971  cshwrepswhash1  16015  divsfval  16406  catsubcat  16697  fthmon  16785  isinitoi  16851  istermoi  16852  iszeroi  16857  setcmon  16935  setcepi  16936  funcestrcsetclem8  16986  fthestrcsetc  16989  funcsetcestrclem8  17001  fthsetcestrc  17004  pltnle  17165  pltval3  17166  lublecllem  17187  latasym  17254  odupos  17334  mrelatglb  17383  mrelatlub  17385  cnvpsb  17412  isgrpid2  17657  ghmghmrn  17875  ghmf1  17885  orbsta  17941  resscntz  17959  gsmsymgrfixlem1  18042  gsmsymgreqlem2  18046  mndodcongi  18157  odf1  18174  lsmss1  18274  lsmss2  18276  efgredeu  18360  cntzcmnss  18441  lt6abl  18491  ablfaclem3  18682  ringinvnz1ne0  18788  kerf1hrm  18941  lspsneq  19323  lspsneu  19324  lsmcv  19343  lidldvgen  19458  0ringnnzr  19472  domnmuln0  19501  opprdomn  19504  ply1scln0  19863  gsummoncoe1  19876  domnchr  20082  znf1o  20101  zntoslem  20106  znfld  20110  cygznlem2a  20117  cygznlem3  20119  islindf4  20381  uvcendim  20390  matvscl  20441  scmataddcl  20527  scmatsubcl  20528  scmatfo  20541  scmatghm  20544  maducoeval2  20651  slesolinv  20692  cramerimplem2  20697  cpmatelimp  20724  cpmatelimp2  20726  cpmatacl  20728  cpmatinvcl  20729  pm2mpf1  20811  cayhamlem1  20878  cayleyhamilton1  20904  0ntr  21083  islpi  21161  lmss  21310  cmpcld  21413  cmpfi  21419  1stcelcls  21472  comppfsc  21543  ptcnplem  21632  qtophmeo  21828  fbdmn0  21845  fbasrn  21895  elfm3  21961  fmfnfmlem4  21968  fclscf  22036  cnpfcf  22052  alexsubALTlem3  22060  tsmsres  22154  blval2  22574  tnggrpr  22666  nmoleub  22742  nmhmcn  23126  ncvs1  23163  iscau4  23283  caussi  23301  cniccbdd  23436  ovoliunnul  23482  mbfinf  23640  itg2splitlem  23723  dvcn  23892  c1lip1  23968  c1lip3  23970  dvcnvrelem1  23988  ply1divex  24104  quotcan  24272  aannenlem1  24291  taylf  24323  ulmcaulem  24356  ulmcau  24357  reeff1o  24409  logccv  24617  logreclem  24708  isosctrlem2  24757  xrlimcnp  24903  rlimcxp  24908  ftalem7  25013  vmappw  25050  fsumvma  25146  dchreq  25191  dchrptlem1  25197  dchrsum  25202  bposlem7  25223  lgsqrlem2  25280  lgsdchr  25288  gausslemma2dlem1a  25298  lgseisenlem2  25309  lgsquad2  25319  2lgslem1b  25325  2sqlem6  25356  tgcgrcomimp  25580  isperp2  25818  xmstrkgc  25974  brbtwn  25987  brcgr  25988  axcgrid  26004  axeuclidlem  26050  axeuclid  26051  lpvtx  26171  upgrex  26195  upgrpredgv  26243  upgredgpr  26246  uhgr0v0e  26340  subgrprop  26375  fusgrfisbase  26430  edgnbusgreu  26478  edgnbusgreuOLD  26479  nbusgredgeu0  26480  cusgredg  26542  structtocusgr  26564  cusgrsize2inds  26571  cusgrsize  26572  usgredgsscusgredg  26577  fusgrmaxsize  26582  uspgrloopvtxel  26634  umgr2v2e  26643  vtxdginducedm1fi  26662  finsumvtxdg2sstep  26667  rgrprop  26678  rusgrprop  26680  0uhgrrusgr  26696  rusgrpropedg  26702  ewlkprop  26721  upgrewlkle2  26724  wlkprop  26729  upgrwlkcompim  26761  uspgr2wlkeq  26764  wlklenvclwlk  26773  wlkonprop  26776  wlkres  26789  redwlk  26791  wlkdlem2  26802  wksonproplem  26823  usgr2trlspth  26879  usgr2pth  26882  pthdlem1  26884  crctcshwlkn0lem4  26928  wwlksnprcl  26954  wlkiswwlks2  26996  wwlksm1edg  27002  wlknewwlksn  27008  wwlksnred  27023  wwlksnext  27024  wwlksnextbi  27025  wwlksnextwrd  27028  wwlksnextinj  27030  wwlksnextsur  27031  umgr2wlk  27083  umgrwwlks2on  27092  elwwlks2  27102  clwwlk1loop  27125  clwwlkccatlem  27126  umgrclwwlkge2  27128  clwlkclwwlklem2a1  27129  clwlkclwwlklem2a4  27134  clwlkclwwlklem2a  27135  clwlkclwwlklem2  27137  clwlkclwwlkfo  27146  clwwisshclwwslemlem  27150  clwwlknwwlksn  27180  clwwlknwwlksnOLD  27181  clwwlknlbonbgr1  27182  clwwlkn1loopb  27186  clwwlkf  27190  wwlksext2clwwlk  27201  wwlksext2clwwlkOLD  27202  clwlksfclwwlkOLD  27230  clwwlknon1  27259  clwwlknonwwlknonb  27268  clwwlknonwwlknonbOLD  27269  clwwlknonex2lem2  27271  vdn0conngrumgrv2  27363  frgrnbnb  27462  frgrncvvdeqlem2  27469  frgrncvvdeqlem3  27470  frgrncvvdeqlem6  27473  frgrwopreglem4a  27479  fusgr2wsp2nb  27503  frrusgrord0lem  27508  numclwwlk2lem1lem  27512  numclwwlk2lem1lemOLD  27513  2clwwlk2clwwlklem  27517  2clwwlk2clwwlk  27521  numclwwlk1lem2foa  27527  numclwwlk1lem2f1  27530  frgrreg  27576  hlipgt0  28092  ocin  28477  ocnel  28479  shmodsi  28570  pjmf1  28897  unopf1o  29097  staddi  29427  stadd3i  29429  mdi  29476  dmdmd  29481  dmdi  29483  dmdbr2  29484  dmdbr3  29486  dmdbr4  29487  dmdi4  29488  mdsl1i  29502  superpos  29535  cvbr4i  29548  atssma  29559  atcv1  29561  atomli  29563  chirredlem1  29571  addltmulALT  29627  bian1d  29628  ifeqeqx  29680  disjxpin  29720  suppss3  29823  fpwrelmap  29829  ogrpaddlt  30037  metider  30256  tpr2rico  30277  xrge0iifiso  30300  qqhcn  30354  qqhucn  30355  esumlub  30441  esumpinfval  30454  esumpinfsum  30458  ballotlemfc0  30873  ballotlemfcc  30874  ftc2re  30995  bnj517  31272  erdsze2lem2  31503  trpredrec  32052  poseq  32068  soseq  32069  sltval2  32124  sltres  32130  nodenselem8  32156  nodense  32157  noresle  32161  scutun12  32232  madeval2  32251  dfrdg4  32373  altopthsn  32383  btwncomim  32435  btwnexch3  32442  btwnexch2  32445  endofsegid  32507  opnrebl2  32631  nn0prpwlem  32632  onsuct0  32751  ordcmp  32757  nndivsub  32767  dnibndlem13  32791  bj-cbvexw  32973  bj-cbv3tb  33020  bj-spimtv  33027  bj-spvv  33032  bj-chvarv  33034  bj-equsal  33120  bj-sbsb  33131  bj-ax8  33189  bj-vtoclf  33211  bj-zfauscl  33226  bj-snsetex  33255  bj-ismooredr2  33370  bj-inftyexpiinj  33407  bj-finsumval0  33458  bj-bary1lem1  33472  bj-bary1  33473  f1omptsnlem  33494  iooelexlt  33520  relowlpssretop  33522  rdgeqoa  33528  finxpsuclem  33544  wl-equsal1i  33637  wl-ax11-lem10  33679  ltflcei  33704  sin2h  33706  cos2h  33707  tan2h  33708  lindsenlbs  33711  matunitlindf  33714  poimirlem3  33719  poimirlem4  33720  poimirlem18  33734  poimirlem20  33736  poimirlem21  33737  poimirlem22  33738  poimirlem24  33740  poimirlem25  33741  poimirlem26  33742  poimirlem27  33743  poimirlem28  33744  poimirlem31  33747  poimir  33749  heicant  33751  mblfinlem1  33753  mblfinlem2  33754  mblfinlem3  33755  mblfinlem4  33756  mbfresfi  33762  cnambfre  33764  ftc1anc  33799  dvasin  33802  areacirclem1  33806  areacirclem4  33809  areacirc  33811  brabg2  33816  fzmul  33842  fdc  33846  incsequz2  33850  isbnd2  33887  opidonOLD  33956  opidon2OLD  33958  grpomndo  33979  elghomlem2OLD  33990  rngoueqz  34044  dvrunz  34058  divrngidl  34132  dral1-o  34677  lsatn0  34773  l1cvpat  34828  leat2  35068  atnle  35091  cvlcvr1  35113  cvrexchlem  35193  cvratlem  35195  cvrat  35196  atcvrj0  35202  atle  35210  snatpsubN  35524  linepsubN  35526  pmapsub  35542  lneq2at  35552  lncvrelatN  35555  2llnma3r  35562  cdlemblem  35567  paddasslem5  35598  poml4N  35727  lhpmcvr4N  35800  trlval2  35938  cdlemd6  35978  cdleme7ga  36023  cdleme25b  36129  cdleme29b  36150  cdleme35fnpq  36224  cdleme50f1  36318  cdlemf1  36336  cdlemg27b  36471  cdlemk28-3  36683  tendospcanN  36798  diaf11N  36824  dia2dimlem1  36839  dibf11N  36936  dihf11  37042  dihmeetlem1N  37065  dochvalr  37132  dochnel2  37167  dvh4dimlem  37218  dochsat0  37232  mapd1o  37423  hdmapf1oN  37640  hgmapval0  37667  hgmapf1oN  37678  hlhilhillem  37735  rexrabdioph  37854  fphpdo  37877  irrapxlem3  37884  rmxypairf1o  37971  rmxycomplete  37977  zindbi  38006  lermxnn0  38012  ltrmy  38014  rmyeq0  38015  rmyeq  38016  lermy  38017  acongsym  38038  acongneg2  38039  wepwsolem  38107  intabssd  38410  ss2iundf  38445  frege129d  38549  frege133d  38551  axfrege52a  38644  axfrege52c  38675  ntrk0kbimka  38831  gneispace  38926  suprleubrd  38960  suprlubrd  38964  radcnvrat  39007  nzss  39010  expgrowthi  39026  ordpss  39147  bi23impib  39183  bi23imp13  39189  rspsbc2  39236  tratrb  39238  sbcim2g  39240  truniALT  39243  3impcombi  39535  tpid3gVD  39565  orbi1rVD  39571  sbc3orgVD  39574  rspsbc2VD  39578  tratrbVD  39585  sbcim2gVD  39599  sbcbiVD  39600  truniALTVD  39602  trintALTVD  39604  trintALT  39605  csbingVD  39608  csbsngVD  39617  csbxpgVD  39618  csbresgVD  39619  csbrngVD  39620  csbima12gALTVD  39621  csbunigVD  39622  csbfv12gALTVD  39623  relopabVD  39625  isosctrlem1ALT  39658  fzisoeu  39989  xrralrecnnge  40086  allbutfi  40089  climinf  40312  liminfreuzlem  40508  climliminf  40512  climliminflimsup  40514  xlimbr  40527  stoweidlem7  40697  stoweidlem62  40752  sge0gerpmpt  41092  meaiuninclem  41170  carageniuncllem2  41212  issmflem  41412  funressnfv  41656  funressnvmo  41658  2reu3  41694  ralbinrald  41705  afv0fv0  41732  afv0nbfvbi  41734  afvfv0bi  41735  fnbrafvb  41737  afvres  41755  tz6.12-afv  41756  afvco2  41759  ndmaovcl  41786  afv2res  41822  tz6.12-afv2  41823  nelbrim  41858  f1oresf1o2  41875  zm1nn  41886  nltle2tri  41892  subsubelfzo0  41905  iccpartres  41923  iccpartiltu  41927  fargshiftfv  41944  pfxfv  41968  pfxsuff1eqwrdeq  41976  reuccatpfxs1lem  42002  fmtnof1  42016  goldbachthlem2  42027  fmtnoprmfac1  42046  fmtnoprmfac2  42048  lighneallem2  42092  lighneallem4b  42095  lighneallem4  42096  evennodd  42125  oddneven  42126  oexpnegnz  42158  evenltle  42195  gbowge7  42220  gbege6  42222  sbgoldbwt  42234  sbgoldbst  42235  nnsum3primesle9  42251  bgoldbtbndlem2  42263  prsprel  42299  sprsymrelf1lem  42303  sprsymrelfolem2  42305  sprsymrelfo  42309  mgmpropd  42337  clintop  42406  isassintop  42408  lidldomn1  42483  uzlidlring  42491  2zrngnmlid2  42513  rngccatidALTV  42551  ringccatidALTV  42614  srhmsubc  42638  srhmsubcALTV  42656  ztprmneprm  42687  pgrpgt2nabl  42709  lindslinindimp2lem4  42812  lincresunit3  42832  fldivexpfllog2  42921  digexp  42963  spd  42987  spcdvw  42988  setrec2fun  43001