Theorem biimpd 228

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

Syntax hints:   → wi 4   ↔ wb 205

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 206

This theorem is referenced by:  mpbid  231  sylibd  238  sylbid  239  mpbidi  240  imbitrid  243  syl6bi  253  con4bid  317  mtbird  325  mtbiri  327  imbi1d  342  bitr3  353  pm5.21im  375  biimpa  478  alexbii  1836  spvv  2001  spfw  2037  cbvalw  2039  sbequi  2088  chvarfv  2234  cbvalv1  2338  spv  2393  chvar  2395  cbval  2398  sb1  2478  nfsb4t  2499  exmoeu  2576  euim  2614  2eu3  2650  eqrdav  2732  ralbida  3268  raleleqOLD  3341  rgen2a  3368  ralcom2  3374  ceqsalt  3506  ceqsalgALT  3509  vtoclfOLD  3549  vtoclegft  3574  spcdv  3585  rspcdv  3605  rspcebdv  3607  rexraleqim  3636  elabgtOLD  3664  sbcn1  3833  sbcim1OLD  3835  sbcbi1  3839  sbeqalb  3846  sbcel21v  3851  disj  4448  elpwunsn  4688  rabsnifsb  4727  ssunsn2  4831  preqr1g  4854  iuneqconst  5009  axprlem3  5424  sbcop1  5489  propeqop  5508  euotd  5514  rexopabb  5529  sotr2  5621  relop  5851  elinxp  6020  elimasni  6091  sotri2  6131  onmindif  6457  iotavalOLD  6518  dffv2  6987  mpteqb  7018  elfvmptrab  7027  chfnrn  7051  elpreima  7060  iinpreima  7071  exfo  7107  ffnfv  7118  f1elima  7262  f1eqcocnv  7299  f1eqcocnvOLD  7300  fliftfun  7309  soisores  7324  isotr  7333  isomin  7334  ovmpodv2  7566  difsnexi  7748  onint  7778  oneqmin  7788  ordunisuc2  7833  tfindsg  7850  findsg  7890  f1oweALT  7959  el2mpocl  8072  poseq  8144  soseq  8145  ressuppss  8168  funsssuppss  8175  suppofssd  8188  smoiso  8362  seqomlem2  8451  oaordi  8546  oawordri  8550  oaordex  8558  oalimcl  8560  omwordi  8571  oewordi  8591  oelim2  8595  nnmwordi  8635  xpider  8782  iiner  8783  undifixp  8928  mptelixpg  8929  dom2lem  8988  findcard2s  9165  pssnn  9168  nneneq  9209  nneneqOLD  9221  fineqvlem  9262  pssnnOLD  9265  dif1ennnALT  9277  unfilem2  9311  xpfiOLD  9318  domunfican  9320  f1dmvrnfibi  9336  fsuppimp  9368  dffi2  9418  infsupprpr  9499  wemaplem2  9542  suc11reg  9614  noinfep  9655  cantnflem1  9684  r1fin  9768  tcrank  9879  cardlim  9967  pr2nelemOLD  9998  fseqenlem1  10019  alephnbtwn  10066  alephord2i  10072  alephf1  10080  cardaleph  10084  alephiso  10093  dfac12lem2  10139  ackbij1lem16  10230  cflm  10245  cfcoflem  10267  sornom  10272  fin23lem27  10323  isf32lem7  10354  fin17  10389  fin1a2lem2  10396  fin1a2lem4  10398  fin1a2lem6  10400  fin1a2lem9  10403  axdc3lem2  10446  zorn2lem7  10497  uniimadom  10539  inar1  10770  grothomex  10824  addcanpi  10894  mulcanpi  10895  enqer  10916  genpcd  11001  genpnmax  11002  ltexprlem4  11034  reclem3pr  11044  reclem4pr  11045  suplem2pr  11048  axpre-ltadd  11162  axpre-sup  11164  ltletr  11306  00id  11389  addn0nid  11634  mul0or  11854  prodgt02  12062  lemul1a  12068  mulgt1  12073  divgt0  12082  divge0  12083  ledivp1i  12139  ltdivp1i  12140  cju  12208  nnsub  12256  nominpos  12449  nn0n0n1ge2  12539  btwnnz  12638  suprfinzcl  12676  ublbneg  12917  zmax  12929  cnref1o  12969  ltsubrp  13010  ltaddrp  13011  xrltletr  13136  qbtwnre  13178  xltnegi  13195  xnn0xadd0  13226  iccsupr  13419  icoshft  13450  difreicc  13461  iccshftri  13464  iccshftli  13466  iccdili  13468  icccntri  13470  fzen  13518  elfz1b  13570  fzofzim  13679  eluzgtdifelfzo  13694  elfzo1elm1fzo0  13733  injresinjlem  13752  injresinj  13753  flval2  13779  flval3  13780  modmuladdim  13879  modaddmodup  13899  addmodlteq  13911  fseqsupubi  13943  ssnn0fi  13950  mptnn0fsuppr  13964  sq01  14188  hashf1rn  14312  hashgt12el  14382  hashgt12el2  14383  hashfundm  14402  hash2pr  14430  hash2exprb  14432  hashge2el2difr  14442  hashtpg  14446  hash3tr  14451  lswlgt0cl  14519  ccatalpha  14543  pfxfv  14632  pfxsuff1eqwrdeq  14649  ccatopth2  14667  swrdccat  14685  swrdccat3blem  14689  reuccatpfxs1lem  14696  repsdf2  14728  repswsymball  14729  repswrevw  14737  cshweqrep  14771  cshw1  14772  2cshwcshw  14776  scshwfzeqfzo  14777  cshwcsh2id  14779  swrdco  14788  swrd2lsw  14903  2swrd2eqwrdeq  14904  wwlktovfo  14909  cjre  15086  icodiamlt  15382  reusq0  15409  o1lo1  15481  o1of2  15557  o1rlimmul  15563  zsum  15664  modfsummods  15739  zprod  15881  reeff1  16063  dvdsmod0  16203  dvds2lem  16212  muldvds1  16224  dvdscmulr  16228  dvdsmulcr  16229  dvdsdivcl  16259  mod2eq1n2dvds  16290  oddnn02np1  16291  divalglem8  16343  ndvdsadd  16353  zeqzmulgcd  16451  dfgcd2  16488  absproddvds  16554  lcmftp  16573  coprmdvds  16590  2mulprm  16630  isprm5  16644  divgcdodd  16647  isprm6  16651  prmdvdsexpr  16654  cncongrprm  16665  phiprmpw  16709  modprm0  16738  pythagtriplem4  16752  pcz  16814  difsqpwdvds  16820  1arith  16860  prmgaplem5  16988  prmgaplem6  16989  cshwrepswhash1  17036  sbcie2s  17094  divsfval  17493  catsubcat  17789  fthmon  17878  isinitoi  17949  istermoi  17950  iszeroi  17959  setcmon  18037  setcepi  18038  funcestrcsetclem8  18099  fthestrcsetc  18102  funcsetcestrclem8  18114  fthsetcestrc  18117  odupos  18281  pltnle  18291  pltval3  18292  lublecllem  18313  latasym  18396  mrelatglb  18513  mrelatlub  18515  cnvpsb  18532  isgrpid2  18861  ghmghmrn  19111  ghmf1  19121  orbsta  19177  resscntz  19197  gsmsymgrfixlem1  19295  gsmsymgreqlem2  19299  mndodcongi  19411  odf1  19430  lsmss1  19533  lsmss2  19535  efgredeu  19620  cntzcmnss  19709  imasabl  19744  lt6abl  19763  ablfaclem3  19957  ringinvnz1ne0  20112  kerf1ghm  20282  0ringnnzr  20302  lspsneq  20735  lspsneu  20736  lsmcv  20754  lidldvgen  20893  domnmuln0  20914  opprdomn  20919  domnchr  21084  znf1o  21107  zntoslem  21112  znfld  21116  cygznlem2a  21123  cygznlem3  21125  phlssphl  21212  islindf4  21393  uvcendim  21402  ply1scln0  21814  gsummoncoe1  21828  matvscl  21933  scmataddcl  22018  scmatsubcl  22019  scmatfo  22032  scmatghm  22035  maducoeval2  22142  slesolinv  22182  cramerimplem2  22186  cpmatelimp  22214  cpmatelimp2  22216  cpmatacl  22218  cpmatinvcl  22219  pm2mpf1  22301  cayhamlem1  22368  cayleyhamilton1  22394  0ntr  22575  islpi  22653  lmss  22802  cmpcld  22906  cmpfi  22912  1stcelcls  22965  comppfsc  23036  ptcnplem  23125  qtophmeo  23321  fbdmn0  23338  fbasrn  23388  elfm3  23454  fmfnfmlem4  23461  fclscf  23529  cnpfcf  23545  alexsubALTlem3  23553  tsmsres  23648  blval2  24071  tnggrpr  24172  nmoleub  24248  nmhmcn  24636  ncvs1  24674  iscau4  24796  caussi  24814  cmssmscld  24867  cmslssbn  24889  cniccbdd  24978  ovoliunnul  25024  mbfinf  25182  itg2splitlem  25266  dvcn  25438  c1lip1  25514  c1lip3  25516  dvcnvrelem1  25534  ply1divex  25654  quotcan  25822  aannenlem1  25841  taylf  25873  ulmcaulem  25906  ulmcau  25907  reeff1o  25959  logccv  26171  logreclem  26267  isosctrlem2  26324  xrlimcnp  26473  rlimcxp  26478  ftalem7  26583  vmappw  26620  fsumvma  26716  dchreq  26761  dchrptlem1  26767  dchrsum  26772  bposlem7  26793  lgsqrlem2  26850  lgsdchr  26858  gausslemma2dlem1a  26868  lgseisenlem2  26879  lgsquad2  26889  2lgslem1b  26895  2sqlem6  26926  2sqnn0  26941  addsq2reu  26943  2sqreulem2  26955  sltval2  27159  sltres  27165  nodenselem8  27194  nodense  27195  noresle  27200  scutun12  27311  madeval2  27348  elmade  27362  negsf1o  27528  recsex  27665  tgcgrcomimp  27728  isperp2  27966  xmstrkgc  28143  brbtwn  28157  brcgr  28158  axcgrid  28174  axeuclidlem  28220  axeuclid  28221  elntg2  28243  lpvtx  28328  upgrex  28352  upgrpredgv  28399  upgredgpr  28402  uhgr0v0e  28495  subgrprop  28530  fusgrfisbase  28585  edgnbusgreu  28624  nbusgredgeu0  28625  cusgredg  28681  structtocusgr  28703  cusgrsize2inds  28710  cusgrsize  28711  usgredgsscusgredg  28716  fusgrmaxsize  28721  uspgrloopvtxel  28773  umgr2v2e  28782  vtxdginducedm1fi  28801  finsumvtxdg2sstep  28806  rgrprop  28817  rusgrprop  28819  0uhgrrusgr  28835  rusgrpropedg  28841  ewlkprop  28860  upgrewlkle2  28863  wlkprop  28868  upgrwlkcompim  28900  uspgr2wlkeq  28903  wlklenvclwlk  28912  wlkonprop  28915  wlkres  28927  redwlk  28929  wlkdlem2  28940  wksonproplem  28961  wksonproplemOLD  28962  usgr2trlspth  29018  usgr2pth  29021  pthdlem1  29023  crctcshwlkn0lem4  29067  wwlksnprcl  29093  wlkiswwlks2  29129  wwlksm1edg  29135  wlknewwlksn  29141  wwlksnred  29146  wwlksnextbi  29148  wwlksnextwrd  29151  wwlksnextinj  29153  wwlksnextsurj  29154  umgr2wlk  29203  umgrwwlks2on  29211  elwwlks2  29220  clwwlk1loop  29241  umgrclwwlkge2  29244  clwlkclwwlklem2a1  29245  clwlkclwwlklem2a4  29250  clwlkclwwlklem2a  29251  clwlkclwwlklem2  29253  clwlkclwwlkfo  29262  clwwisshclwwslemlem  29266  clwwlknwwlksn  29291  clwwlknlbonbgr1  29292  clwwlkn1loopb  29296  clwwlkf  29300  clwwlknon1  29350  clwwlknonwwlknonb  29359  clwwlknonex2lem2  29361  vdn0conngrumgrv2  29449  frgrnbnb  29546  frgrncvvdeqlem2  29553  frgrncvvdeqlem3  29554  frgrncvvdeqlem6  29557  frgrwopreglem4a  29563  fusgr2wsp2nb  29587  frrusgrord0lem  29592  numclwwlk2lem1lem  29595  2clwwlk2clwwlklem  29599  2clwwlk2clwwlk  29603  numclwwlk1lem2foa  29607  numclwwlk1lem2f1  29610  frgrreg  29647  hlipgt0  30167  ocin  30549  ocnel  30551  shmodsi  30642  pjmf1  30969  unopf1o  31169  staddi  31499  stadd3i  31501  mdi  31548  dmdmd  31553  dmdi  31555  dmdbr2  31556  dmdbr3  31558  dmdbr4  31559  dmdi4  31560  mdsl1i  31574  superpos  31607  cvbr4i  31620  atssma  31631  atcv1  31633  atomli  31635  chirredlem1  31643  addltmulALT  31699  bian1d  31700  ifeqeqx  31774  disjxpin  31819  suppss3  31949  fpwrelmap  31958  prmdvdsbc  32022  ogrpaddlt  32235  qsfld  32612  ply1degltdimlem  32707  ply1degltdim  32708  metider  32874  tpr2rico  32892  xrge0iifiso  32915  qqhcn  32971  qqhucn  32972  esumlub  33058  esumpinfval  33071  esumpinfsum  33075  ballotlemfc0  33491  ballotlemfcc  33492  ftc2re  33610  bnj517  33896  fnrelpredd  34092  pfxwlk  34114  subgrwlk  34123  loop1cycl  34128  erdsze2lem2  34195  satfv1  34354  satfdmlem  34359  satf0op  34368  fmlasuc  34377  dfrdg4  34923  altopthsn  34933  btwncomim  34985  btwnexch3  34992  btwnexch2  34995  endofsegid  35057  gg-negcncf  35166  gg-dvfsumlem2  35183  opnrebl2  35206  nn0prpwlem  35207  onsuct0  35326  ordcmp  35332  nndivsub  35342  dnibndlem13  35366  bj-cbval  35526  bj-cbvex  35527  bj-cbvexw  35553  bj-cbv3tb  35665  bj-spimtv  35672  bj-equsal  35704  bj-sbsb  35715  bj-vtoclf  35795  bj-zfauscl  35804  bj-gabss  35815  bj-gabeqd  35817  currysetlem2  35829  bj-snsetex  35844  bj-ismooredr2  35991  bj-inftyexpiinj  36090  bj-finsumval0  36166  bj-fvimacnv0  36167  bj-bary1lem1  36192  bj-bary1  36193  f1omptsnlem  36217  iooelexlt  36243  relowlpssretop  36245  rdgeqoa  36251  finxpsuclem  36278  fvineqsneq  36293  pibt2  36298  wl-equsal1i  36412  wl-ax11-lem10  36456  ltflcei  36476  sin2h  36478  cos2h  36479  tan2h  36480  lindsenlbs  36483  matunitlindf  36486  poimirlem3  36491  poimirlem4  36492  poimirlem18  36506  poimirlem20  36508  poimirlem21  36509  poimirlem22  36510  poimirlem24  36512  poimirlem25  36513  poimirlem26  36514  poimirlem27  36515  poimirlem28  36516  poimirlem31  36519  poimir  36521  heicant  36523  mblfinlem1  36525  mblfinlem2  36526  mblfinlem3  36527  mblfinlem4  36528  mbfresfi  36534  cnambfre  36536  ftc1anc  36569  dvasin  36572  areacirclem1  36576  areacirclem4  36579  areacirc  36581  brabg2  36585  fzmul  36609  fdc  36613  incsequz2  36617  isbnd2  36651  opidonOLD  36720  opidon2OLD  36722  grpomndo  36743  elghomlem2OLD  36754  rngoueqz  36808  dvrunz  36822  divrngidl  36896  refressn  37313  dral1-o  37774  lsatn0  37869  l1cvpat  37924  leat2  38164  atnle  38187  cvlcvr1  38209  cvrexchlem  38290  cvratlem  38292  cvrat  38293  atcvrj0  38299  atle  38307  snatpsubN  38621  linepsubN  38623  pmapsub  38639  lneq2at  38649  lncvrelatN  38652  2llnma3r  38659  cdlemblem  38664  paddasslem5  38695  poml4N  38824  lhpmcvr4N  38897  trlval2  39034  cdlemd6  39074  cdleme7ga  39119  cdleme25b  39225  cdleme29b  39246  cdleme35fnpq  39320  cdleme50f1  39414  cdlemf1  39432  cdlemg27b  39567  cdlemk28-3  39779  tendospcanN  39894  diaf11N  39920  dia2dimlem1  39935  dibf11N  40032  dihf11  40138  dihmeetlem1N  40161  dochvalr  40228  dochnel2  40263  dvh4dimlem  40314  dochsat0  40328  mapd1o  40519  hdmapf1oN  40736  hgmapval0  40763  hgmapf1oN  40774  hlhilhillem  40835  nnproddivdvdsd  40866  lcmineqlem  40917  aks4d1p1p5  40940  aks4d1p3  40943  aks4d1p8d2  40950  aks4d1p8  40952  aks4d1p9  40953  fldhmf1  40955  aks6d1c2p2  40957  sticksstones1  40962  sticksstones3  40964  sticksstones8  40969  sticksstones11  40972  sticksstones12  40974  sticksstones20  40982  sticksstones22  40984  metakunt7  40991  sn-axprlem3  41034  frlmsnic  41110  fsuppind  41162  oexpreposd  41212  rtprmirr  41237  prjspval  41345  rexrabdioph  41532  fphpdo  41555  irrapxlem3  41562  rmxypairf1o  41650  rmxycomplete  41656  zindbi  41685  lermxnn0  41689  ltrmy  41691  rmyeq0  41692  rmyeq  41693  lermy  41694  acongsym  41715  acongneg2  41716  wepwsolem  41784  onsupuni  41978  onsupmaxb  41988  onsucf1o  42022  onov0suclim  42024  oe0suclim  42027  onsucwordi  42038  cantnfresb  42074  omabs2  42082  tfsconcat0b  42096  tfsconcatrev  42098  naddcnffo  42114  oaun3lem1  42124  oaltom  42156  omltoe  42158  sdomne0  42164  sdomne0d  42165  safesnsupfidom1o  42168  intabssd  42270  iscard4  42284  ss2iundf  42410  frege129d  42514  frege133d  42516  axfrege52a  42607  axfrege52c  42638  ntrk0kbimka  42790  gneispace  42885  suprleubrd  42918  suprlubrd  42920  radcnvrat  43073  nzss  43076  expgrowthi  43092  ordpss  43210  bi23impib  43246  bi23imp13  43252  rspsbc2  43295  tratrb  43297  sbcim2g  43299  truniALT  43302  3impcombi  43578  tpid3gVD  43603  orbi1rVD  43609  sbc3orgVD  43612  rspsbc2VD  43616  tratrbVD  43622  sbcim2gVD  43636  sbcbiVD  43637  truniALTVD  43639  trintALTVD  43641  trintALT  43642  csbingVD  43645  csbsngVD  43654  csbxpgVD  43655  csbresgVD  43656  csbrngVD  43657  csbima12gALTVD  43658  csbunigVD  43659  csbfv12gALTVD  43660  relopabVD  43662  isosctrlem1ALT  43695  fzisoeu  44010  xrralrecnnge  44100  allbutfi  44103  climinf  44322  liminfreuzlem  44518  climliminf  44522  climliminflimsup  44524  xlimpnfxnegmnf  44530  xlimbr  44543  stoweidlem7  44723  stoweidlem62  44778  sge0gerpmpt  45118  meaiuninclem  45196  carageniuncllem2  45238  issmflem  45443  et-sqrtnegnre  45589  natlocalincr  45590  tworepnotupword  45600  funressnfv  45753  funressnvmo  45755  f1cof1b  45785  2reu3  45818  ralbinrald  45830  afv0fv0  45857  afv0nbfvbi  45859  afvfv0bi  45860  fnbrafvb  45862  afvres  45880  tz6.12-afv  45881  afvco2  45884  ndmaovcl  45911  afv2res  45947  tz6.12-afv2  45948  nelbrim  45983  f1oresf1o2  45999  zm1nn  46010  nltle2tri  46021  subsubelfzo0  46034  iccpartres  46086  iccpartiltu  46090  fargshiftfv  46107  ichnreuop  46140  ichreuopeq  46141  prsprel  46155  sprsymrelf1lem  46159  sprsymrelfolem2  46161  sprsymrelfo  46165  prpair  46169  paireqne  46179  sbcpr  46189  fmtnof1  46203  goldbachthlem2  46214  fmtnoprmfac1  46233  fmtnoprmfac2  46235  lighneallem2  46274  lighneallem4b  46277  lighneallem4  46278  evennodd  46311  oddneven  46312  oexpnegnz  46346  evenltle  46385  fpprwppr  46407  fpprwpprb  46408  gbowge7  46431  gbege6  46433  sbgoldbwt  46445  sbgoldbst  46446  nnsum3primesle9  46462  bgoldbtbndlem2  46474  isomuspgrlem1  46495  isomuspgrlem2b  46497  isomuspgrlem2c  46498  isomuspgrlem2d  46499  mgmpropd  46545  clintop  46618  isassintop  46620  subrngringnsg  46732  rnglidlmcl  46748  rngqiprngimf1lem  46779  lidldomn1  46823  uzlidlring  46827  2zrngnmlid2  46849  rngccatidALTV  46887  ringccatidALTV  46950  srhmsubc  46974  srhmsubcALTV  46992  ztprmneprm  47023  pgrpgt2nabl  47042  lindslinindimp2lem4  47142  lincresunit3  47162  fldivexpfllog2  47251  digexp  47293  naryfvalelfv  47318  affinecomb1  47388  eenglngeehlnmlem1  47423  eenglngeehlnmlem2  47424  eenglngeehlnm  47425  itscnhlc0yqe  47445  itsclc0yqsol  47450  itscnhlc0xyqsol  47451  itschlc0xyqsol1  47452  itschlc0xyqsol  47453  itsclquadeu  47463  inlinecirc02plem  47472  inlinecirc02p  47473  pm4.71da  47475  mofsn  47510  seposep  47558  idmon  47636  idepi  47637  prsthinc  47674  grptcmon  47716  grptcepi  47717  spd  47723  spcdvw  47724  setrec2fun  47737