Theorem biimpd 221

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

Syntax hints:   → wi 4   ↔ wb 198

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 199

This theorem is referenced by:  mpbid  224  sylibd  231  sylbid  232  mpbidi  233  syl5ib  236  syl6bi  245  ibi  259  con4bid  309  mtbird  317  mtbiri  319  imbi1d  334  bitr3  345  pm5.21im  367  biimpa  469  alexbii  1795  spvv  1955  spfw  1990  cbvalw  1992  alcomiw  1995  sbequi  2036  sbbidOLD  2175  cbvalv1  2277  spimtOLD  2317  spv  2324  chvar  2326  cbval  2329  sb4OLD  2426  sbbidvOLD  2437  nfsb4t  2460  nfsb4tALT  2531  exmoeu  2600  2eu3  2684  2eu3OLD  2685  eqrdav  2777  pm13.18  3048  rgen2a  3176  ralcom2  3304  raleleq  3367  ceqsalgALT  3451  vtoclf  3477  vtocl  3478  vtocl2OLD  3481  spcdv  3512  rspcdv  3538  rspcebdv  3540  rexraleqim  3555  elabgt  3577  sbcn1  3728  sbcim1  3729  sbcbi1  3733  sbeqalb  3739  sbcel21v  3745  elpwunsn  4495  rabsnifsb  4532  ssunsn2  4634  preqr1g  4657  axprlem3  5182  sbcop1  5236  propeqop  5253  euotd  5259  sotr2  5357  relop  5571  elinxp  5735  elimasni  5796  sotri2  5829  relcnvtr  5958  onmindif  6118  iotaval  6163  dffv2  6584  mpteqb  6613  elfvmptrab  6621  chfnrn  6644  elpreima  6653  iinpreima  6662  exfo  6694  ffnfv  6705  f1elima  6846  f1eqcocnv  6882  fliftfun  6888  soisores  6903  isotr  6912  isomin  6913  ovmpodv2  7124  difsnexi  7300  onint  7326  oneqmin  7336  ordunisuc2  7375  tfindsg  7391  findsg  7424  f1oweALT  7485  el2mpocl  7589  ressuppss  7652  funsssuppss  7659  suppofssd  7670  imacosuppOLD  7678  smoiso  7803  seqomlem2  7890  oaordi  7973  oawordri  7977  oaordex  7985  oalimcl  7987  omwordi  7998  oewordi  8018  oelim2  8022  nnmwordi  8062  xpider  8168  iiner  8169  undifixp  8295  mptelixpg  8296  dom2lem  8346  nneneq  8496  fineqvlem  8527  pssnn  8531  dif1en  8546  findcard2s  8554  unfilem2  8578  xpfi  8584  domunfican  8586  f1dmvrnfibi  8603  fsuppimp  8634  dffi2  8682  infsupprpr  8763  wemaplem2  8806  suc11reg  8876  noinfep  8917  cantnflem1  8946  r1fin  8996  tcrank  9107  cardlim  9195  pr2nelem  9224  fseqenlem1  9244  alephnbtwn  9291  alephord2i  9297  alephf1  9305  cardaleph  9309  alephiso  9318  dfac12lem2  9364  ackbij1lem16  9455  cflm  9470  cfcoflem  9492  sornom  9497  fin23lem27  9548  isf32lem7  9579  fin17  9614  fin1a2lem2  9621  fin1a2lem4  9623  fin1a2lem6  9625  fin1a2lem9  9628  axdc3lem2  9671  zorn2lem7  9722  uniimadom  9764  inar1  9995  grothomex  10049  addcanpi  10119  mulcanpi  10120  enqer  10141  genpcd  10226  genpnmax  10227  ltexprlem4  10259  reclem3pr  10269  reclem4pr  10270  suplem2pr  10273  axpre-ltadd  10387  axpre-sup  10389  ltletr  10532  00id  10615  addn0nid  10861  mul0or  11081  prodgt02  11289  lemul1a  11295  mulgt1  11300  divgt0  11309  divge0  11310  ledivp1i  11366  ltdivp1i  11367  cju  11435  nnsub  11484  nominpos  11684  nn0n0n1ge2  11774  btwnnz  11871  suprfinzcl  11910  ublbneg  12147  zmax  12159  cnref1o  12199  ltsubrp  12242  ltaddrp  12243  xrltletr  12367  qbtwnre  12409  xltnegi  12426  xnn0xadd0  12456  iccsupr  12646  icoshft  12675  difreicc  12686  iccshftri  12689  iccshftli  12691  iccdili  12693  icccntri  12695  fzen  12740  elfz1b  12792  fzofzim  12899  eluzgtdifelfzo  12914  elfzo1elm1fzo0  12953  injresinjlem  12972  injresinj  12973  flval2  12999  flval3  13000  modmuladdim  13097  modaddmodup  13117  addmodlteq  13129  fseqsupubi  13161  ssnn0fi  13168  mptnn0fsuppr  13182  sq01  13401  hashf1rn  13528  hashgt12el  13596  hashgt12el2  13597  hash2pr  13638  hash2exprb  13640  hashge2el2difr  13650  hashtpg  13654  hash3tr  13659  lswlgt0cl  13732  ccatalpha  13756  2swrd1eqwrdeqOLD  13847  pfxfv  13864  pfxsuff1eqwrdeq  13881  ccatopth2  13909  reuccats1lemOLD  13920  swrdccatin2  13929  swrdccat  13938  swrdccatOLD  13939  swrdccat3aOLD  13943  swrdccat3blem  13944  reuccatpfxs1lem  13955  repsdf2  13997  repswsymball  13998  repswrevw  14006  cshweqrep  14045  cshw1  14046  2cshwcshw  14049  scshwfzeqfzo  14050  cshwcsh2id  14052  swrdco  14061  swrd2lsw  14176  2swrd2eqwrdeq  14177  2swrd2eqwrdeqOLD  14178  wwlktovfo  14183  cjre  14359  icodiamlt  14656  reusq0  14683  o1lo1  14755  o1of2  14830  o1rlimmul  14836  zsum  14935  modfsummods  15008  zprod  15151  reeff1  15333  dvdsmod0  15473  dvds2lem  15482  muldvds1  15494  dvdscmulr  15498  dvdsmulcr  15499  dvdsdivcl  15526  mod2eq1n2dvds  15556  oddnn02np1  15557  divalglem8  15611  ndvdsadd  15621  zeqzmulgcd  15719  dfgcd2  15750  gcdmultiple  15756  absproddvds  15817  lcmftp  15836  coprmdvds  15853  2mulprm  15893  isprm5  15907  divgcdodd  15910  isprm6  15914  prmdvdsexpr  15917  cncongrprm  15925  phiprmpw  15969  modprm0  15998  pythagtriplem4  16012  pcz  16073  difsqpwdvds  16079  1arith  16119  prmgaplem5  16247  prmgaplem6  16248  cshwrepswhash1  16292  divsfval  16676  catsubcat  16967  fthmon  17055  isinitoi  17121  istermoi  17122  iszeroi  17127  setcmon  17205  setcepi  17206  funcestrcsetclem8  17255  fthestrcsetc  17258  funcsetcestrclem8  17270  fthsetcestrc  17273  pltnle  17434  pltval3  17435  lublecllem  17456  latasym  17523  odupos  17603  mrelatglb  17652  mrelatlub  17654  cnvpsb  17681  isgrpid2  17927  ghmghmrn  18148  ghmf1  18158  orbsta  18214  resscntz  18233  gsmsymgrfixlem1  18316  gsmsymgreqlem2  18320  mndodcongi  18433  odf1  18450  lsmss1  18550  lsmss2  18552  efgredeu  18638  cntzcmnss  18719  lt6abl  18769  ablfaclem3  18959  ringinvnz1ne0  19065  kerf1ghm  19220  kerf1hrmOLD  19221  lspsneq  19616  lspsneu  19617  lsmcv  19635  lidldvgen  19749  0ringnnzr  19763  domnmuln0  19792  opprdomn  19795  ply1scln0  20162  gsummoncoe1  20175  domnchr  20381  znf1o  20400  zntoslem  20405  znfld  20409  cygznlem2a  20416  cygznlem3  20418  phlssphl  20505  islindf4  20684  uvcendim  20693  matvscl  20744  scmataddcl  20829  scmatsubcl  20830  scmatfo  20843  scmatghm  20846  maducoeval2  20953  slesolinv  20993  cramerimplem2  20997  cpmatelimp  21024  cpmatelimp2  21026  cpmatacl  21028  cpmatinvcl  21029  pm2mpf1  21111  cayhamlem1  21178  cayleyhamilton1  21204  0ntr  21383  islpi  21461  lmss  21610  cmpcld  21714  cmpfi  21720  1stcelcls  21773  comppfsc  21844  ptcnplem  21933  qtophmeo  22129  fbdmn0  22146  fbasrn  22196  elfm3  22262  fmfnfmlem4  22269  fclscf  22337  cnpfcf  22353  alexsubALTlem3  22361  tsmsres  22455  blval2  22875  tnggrpr  22967  nmoleub  23043  nmhmcn  23427  ncvs1  23464  iscau4  23585  caussi  23603  cmssmscld  23656  cmslssbn  23678  cniccbdd  23765  ovoliunnul  23811  mbfinf  23969  itg2splitlem  24052  dvcn  24221  c1lip1  24297  c1lip3  24299  dvcnvrelem1  24317  ply1divex  24433  quotcan  24601  aannenlem1  24620  taylf  24652  ulmcaulem  24685  ulmcau  24686  reeff1o  24738  logccv  24947  logreclem  25041  isosctrlem2  25098  xrlimcnp  25248  rlimcxp  25253  ftalem7  25358  vmappw  25395  fsumvma  25491  dchreq  25536  dchrptlem1  25542  dchrsum  25547  bposlem7  25568  lgsqrlem2  25625  lgsdchr  25633  gausslemma2dlem1a  25643  lgseisenlem2  25654  lgsquad2  25664  2lgslem1b  25670  2sqlem6  25701  2sqnn0  25716  addsq2reu  25718  2sqreulem2  25730  tgcgrcomimp  25965  isperp2  26203  xmstrkgc  26375  brbtwn  26388  brcgr  26389  axcgrid  26405  axeuclidlem  26451  axeuclid  26452  elntg2  26474  lpvtx  26556  upgrex  26580  upgrpredgv  26627  upgredgpr  26630  uhgr0v0e  26723  subgrprop  26758  fusgrfisbase  26813  edgnbusgreu  26852  nbusgredgeu0  26853  cusgredg  26909  structtocusgr  26931  cusgrsize2inds  26938  cusgrsize  26939  usgredgsscusgredg  26944  fusgrmaxsize  26949  uspgrloopvtxel  27001  umgr2v2e  27010  vtxdginducedm1fi  27029  finsumvtxdg2sstep  27034  rgrprop  27045  rusgrprop  27047  0uhgrrusgr  27063  rusgrpropedg  27069  ewlkprop  27088  upgrewlkle2  27091  wlkprop  27096  upgrwlkcompim  27127  uspgr2wlkeq  27130  wlklenvclwlk  27139  wlkonprop  27142  wlkres  27156  wlkresOLD  27158  redwlk  27160  wlkdlem2  27171  wksonproplem  27194  usgr2trlspth  27250  usgr2pth  27253  pthdlem1  27255  crctcshwlkn0lem4  27299  wwlksnprcl  27325  wlkiswwlks2  27361  wwlksm1edg  27367  wwlksm1edgOLD  27368  wlknewwlksn  27374  wwlksnred  27379  wwlksnredOLD  27380  wwlksnext  27381  wwlksnextbi  27382  wwlksnextbiOLD  27383  wwlksnextwrd  27388  wwlksnextinj  27390  wwlksnextsurj  27391  wwlksnextwrdOLD  27393  wwlksnextinjOLD  27395  wwlksnextsurOLD  27396  umgr2wlk  27455  umgrwwlks2on  27463  elwwlks2  27472  clwwlk1loop  27494  clwwlkccatlem  27495  umgrclwwlkge2  27497  clwlkclwwlklem2a1  27498  clwlkclwwlklem2a4  27503  clwlkclwwlklem2a  27504  clwlkclwwlklem2  27506  clwlkclwwlkfoOLD  27519  clwlkclwwlkfo  27523  clwwisshclwwslemlem  27528  clwwlknwwlksn  27553  clwwlknlbonbgr1  27554  clwwlkn1loopb  27559  clwwlkfOLD  27564  clwwlkf  27569  wwlksext2clwwlk  27580  clwwlknon1  27625  clwwlknonwwlknonb  27634  clwwlknonex2lem2  27636  vdn0conngrumgrv2  27725  frgrnbnb  27827  frgrncvvdeqlem2  27834  frgrncvvdeqlem3  27835  frgrncvvdeqlem6  27838  frgrwopreglem4a  27844  fusgr2wsp2nb  27868  frrusgrord0lem  27873  numclwwlk2lem1lem  27876  2clwwlk2clwwlklem  27883  2clwwlk2clwwlk  27887  2clwwlk2clwwlkOLD  27888  numclwwlk1lem2foa  27895  numclwwlk1lem2foaOLD  27896  numclwwlk1lem2f1  27899  numclwwlk1lem2f1OLD  27904  frgrreg  27951  hlipgt0  28469  ocin  28854  ocnel  28856  shmodsi  28947  pjmf1  29274  unopf1o  29474  staddi  29804  stadd3i  29806  mdi  29853  dmdmd  29858  dmdi  29860  dmdbr2  29861  dmdbr3  29863  dmdbr4  29864  dmdi4  29865  mdsl1i  29879  superpos  29912  cvbr4i  29925  atssma  29936  atcv1  29938  atomli  29940  chirredlem1  29948  addltmulALT  30004  bian1d  30005  ifeqeqx  30065  disjxpin  30104  suppss3  30219  fpwrelmap  30228  prmdvdsbc  30285  ogrpaddlt  30443  metider  30784  tpr2rico  30805  xrge0iifiso  30828  qqhcn  30882  qqhucn  30883  esumlub  30969  esumpinfval  30982  esumpinfsum  30986  ballotlemfc0  31402  ballotlemfcc  31403  ftc2re  31523  bnj517  31810  erdsze2lem2  32042  satf0op  32193  fmlasuc  32202  trpredrec  32604  poseq  32622  soseq  32623  sltval2  32690  sltres  32696  nodenselem8  32722  nodense  32723  noresle  32727  scutun12  32798  madeval2  32817  dfrdg4  32939  altopthsn  32949  btwncomim  33001  btwnexch3  33008  btwnexch2  33011  endofsegid  33073  opnrebl2  33196  nn0prpwlem  33197  onsuct0  33315  ordcmp  33321  nndivsub  33331  dnibndlem13  33355  bj-cbval  33496  bj-cbvex  33497  bj-cbvexw  33525  bj-cbv3tb  33570  bj-spimtv  33577  bj-chvarv  33579  bj-equsal  33646  bj-sbsb  33657  bj-vtoclf  33729  bj-zfauscl  33744  currysetlem2  33760  bj-snsetex  33799  bj-elep  33875  bj-ismooredr2  33919  bj-inftyexpiinj  33966  bj-finsumval0  34036  bj-bary1lem1  34046  bj-bary1  34047  f1omptsnlem  34065  iooelexlt  34091  relowlpssretop  34093  rdgeqoa  34099  finxpsuclem  34125  fvineqsneq  34140  pibt2  34145  wl-equsal1i  34231  wl-ax11-lem10  34273  ltflcei  34327  sin2h  34329  cos2h  34330  tan2h  34331  lindsenlbs  34334  matunitlindf  34337  poimirlem3  34342  poimirlem4  34343  poimirlem18  34357  poimirlem20  34359  poimirlem21  34360  poimirlem22  34361  poimirlem24  34363  poimirlem25  34364  poimirlem26  34365  poimirlem27  34366  poimirlem28  34367  poimirlem31  34370  poimir  34372  heicant  34374  mblfinlem1  34376  mblfinlem2  34377  mblfinlem3  34378  mblfinlem4  34379  mbfresfi  34385  cnambfre  34387  ftc1anc  34422  dvasin  34425  areacirclem1  34429  areacirclem4  34432  areacirc  34434  brabg2  34439  fzmul  34464  fdc  34468  incsequz2  34472  isbnd2  34509  opidonOLD  34578  opidon2OLD  34580  grpomndo  34601  elghomlem2OLD  34612  rngoueqz  34666  dvrunz  34680  divrngidl  34754  dral1-o  35491  lsatn0  35586  l1cvpat  35641  leat2  35881  atnle  35904  cvlcvr1  35926  cvrexchlem  36006  cvratlem  36008  cvrat  36009  atcvrj0  36015  atle  36023  snatpsubN  36337  linepsubN  36339  pmapsub  36355  lneq2at  36365  lncvrelatN  36368  2llnma3r  36375  cdlemblem  36380  paddasslem5  36411  poml4N  36540  lhpmcvr4N  36613  trlval2  36750  cdlemd6  36790  cdleme7ga  36835  cdleme25b  36941  cdleme29b  36962  cdleme35fnpq  37036  cdleme50f1  37130  cdlemf1  37148  cdlemg27b  37283  cdlemk28-3  37495  tendospcanN  37610  diaf11N  37636  dia2dimlem1  37651  dibf11N  37748  dihf11  37854  dihmeetlem1N  37877  dochvalr  37944  dochnel2  37979  dvh4dimlem  38030  dochsat0  38044  mapd1o  38235  hdmapf1oN  38452  hgmapval0  38479  hgmapf1oN  38490  hlhilhillem  38547  sn-axprlem3  38560  frlmsnic  38592  oexpreposd  38617  rtprmirr  38632  prjspval  38666  rexrabdioph  38793  fphpdo  38816  irrapxlem3  38823  rmxypairf1o  38910  rmxycomplete  38916  zindbi  38945  lermxnn0  38949  ltrmy  38951  rmyeq0  38952  rmyeq  38953  lermy  38954  acongsym  38975  acongneg2  38976  wepwsolem  39044  intabssd  39338  ss2iundf  39373  frege129d  39477  frege133d  39479  axfrege52a  39571  axfrege52c  39602  ntrk0kbimka  39758  gneispace  39853  suprleubrd  39887  suprlubrd  39891  radcnvrat  40068  nzss  40071  expgrowthi  40087  ordpss  40208  bi23impib  40244  bi23imp13  40250  rspsbc2  40293  tratrb  40295  sbcim2g  40297  truniALT  40300  3impcombi  40576  tpid3gVD  40601  orbi1rVD  40607  sbc3orgVD  40610  rspsbc2VD  40614  tratrbVD  40620  sbcim2gVD  40634  sbcbiVD  40635  truniALTVD  40637  trintALTVD  40639  trintALT  40640  csbingVD  40643  csbsngVD  40652  csbxpgVD  40653  csbresgVD  40654  csbrngVD  40655  csbima12gALTVD  40656  csbunigVD  40657  csbfv12gALTVD  40658  relopabVD  40660  isosctrlem1ALT  40693  fzisoeu  41002  xrralrecnnge  41098  allbutfi  41101  climinf  41324  liminfreuzlem  41520  climliminf  41524  climliminflimsup  41526  xlimpnfxnegmnf  41532  xlimbr  41545  stoweidlem7  41729  stoweidlem62  41784  sge0gerpmpt  42121  meaiuninclem  42199  carageniuncllem2  42241  issmflem  42441  funressnfv  42689  funressnvmo  42691  funressnvmoOLD  42692  2reu3  42721  ralbinrald  42733  afv0fv0  42760  afv0nbfvbi  42762  afvfv0bi  42763  fnbrafvb  42765  afvres  42783  tz6.12-afv  42784  afvco2  42787  ndmaovcl  42814  afv2res  42850  tz6.12-afv2  42851  nelbrim  42886  f1oresf1o2  42902  zm1nn  42914  nltle2tri  42925  subsubelfzo0  42938  iccpartres  42956  iccpartiltu  42960  fargshiftfv  42977  ichan  43004  ichnreuop  43008  ichreuopeq  43009  prsprel  43023  sprsymrelf1lem  43027  sprsymrelfolem2  43029  sprsymrelfo  43033  prpair  43037  paireqne  43047  sbcpr  43057  fmtnof1  43071  goldbachthlem2  43082  fmtnoprmfac1  43101  fmtnoprmfac2  43103  lighneallem2  43145  lighneallem4b  43148  lighneallem4  43149  evennodd  43182  oddneven  43183  oexpnegnz  43217  evenltle  43256  fpprwppr  43278  fpprwpprb  43279  gbowge7  43302  gbege6  43304  sbgoldbwt  43316  sbgoldbst  43317  nnsum3primesle9  43333  bgoldbtbndlem2  43345  isomuspgrlem1  43366  isomuspgrlem2b  43368  isomuspgrlem2c  43369  isomuspgrlem2d  43370  mgmpropd  43416  clintop  43485  isassintop  43487  lidldomn1  43562  uzlidlring  43570  2zrngnmlid2  43592  rngccatidALTV  43630  ringccatidALTV  43693  srhmsubc  43717  srhmsubcALTV  43735  ztprmneprm  43765  pgrpgt2nabl  43786  lindslinindimp2lem4  43889  lincresunit3  43909  fldivexpfllog2  43999  digexp  44041  affinecomb1  44063  eenglngeehlnmlem1  44098  eenglngeehlnmlem2  44099  eenglngeehlnm  44100  itscnhlc0yqe  44120  itsclc0yqsol  44125  itscnhlc0xyqsol  44126  itschlc0xyqsol1  44127  itschlc0xyqsol  44128  itsclquadeu  44138  inlinecirc02plem  44147  inlinecirc02p  44148  spd  44154  spcdvw  44155  setrec2fun  44168