Theorem syl5bi 232

Description: A mixed syllogism inference from a nested implication and a biconditional. Useful for substituting an embedded antecedent with a definition. (Contributed by NM, 12-Jan-1993.)

Hypotheses

Ref	Expression
syl5bi.1	⊢ (𝜑 ↔ 𝜓)
syl5bi.2	⊢ (𝜒 → (𝜓 → 𝜃))

Assertion

Ref	Expression
syl5bi	⊢ (𝜒 → (𝜑 → 𝜃))

Proof of Theorem syl5bi

Step	Hyp	Ref	Expression
1		syl5bi.1	. . 3 ⊢ (𝜑 ↔ 𝜓)
2	1	biimpi 206	. 2 ⊢ (𝜑 → 𝜓)
3		syl5bi.2	. 2 ⊢ (𝜒 → (𝜓 → 𝜃))
4	2, 3	syl5 34	1 ⊢ (𝜒 → (𝜑 → 𝜃))

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:  3imtr4g  285  ancomsd  470  3orel1  1041  3jao  1389  nfimdOLDOLD  1824  axc16nf  2137  ax13  2249  2euex  2544  2eu1  2553  eqneqall  2805  necon3bd  2808  pm2.61dne  2880  elnelall  2910  spcimgft  3284  rspc  3303  rspcimdv  3310  rspc2gv  3321  euind  3393  reuind  3411  sbciegft  3466  rspsbc  3518  ssexnelpss  3720  ralnralall  4080  pwpw0  4344  sssn  4358  eqsnOLD  4362  prel12  4383  prnebg  4389  pwsnALT  4429  intss1  4492  intmin  4497  uniintsn  4514  iinss  4571  iinss2  4572  disji2  4636  disjiun  4640  disjiund  4643  disjxiun  4649  disjxiunOLD  4650  trel3  4760  trin  4763  trintssOLD  4770  eusvnfb  4862  reusv3  4876  copsexg  4956  propeqop  4970  otiunsndisj  4980  iunopeqop  4981  po3nr  5049  fri  5076  wefrc  5108  wereu2  5111  ssrelrel  5220  relop  5272  iss  5447  restidsingOLD  5459  poirr2  5520  xpcan  5570  xpcan2  5571  sossfld  5580  wfi  5713  wfis2fg  5717  onfr  5763  onmindif  5815  funopg  5922  funssres  5930  funun  5932  fv3  6206  fvmptt  6300  iinpreima  6345  fvn0ssdmfun  6350  dff3  6372  dff4  6373  fmptsng  6434  fmptsnd  6435  tpres  6466  fnprb  6472  fntpb  6473  fvclss  6500  fpropnf1  6524  isomin  6587  isofrlem  6590  weniso  6604  oprabid  6677  ssorduni  6985  onmindif2  7012  limuni3  7052  tfis2f  7055  tfinds  7059  tfinds2  7063  tfinds3  7064  funcnvuni  7119  f1oweALT  7152  f1o2ndf1  7285  poxp  7289  soxp  7290  fnse  7294  suppimacnv  7306  mpt2xopynvov0g  7340  reldmtpos  7360  rntpos  7365  wfrlem14  7428  wfrlem15  7429  onfununi  7438  smoiun  7458  tfrlem1  7472  tfr3  7495  frsucmptn  7534  tz7.49  7540  oaordi  7626  oawordeulem  7634  omeulem1  7662  oeordi  7667  oelimcl  7680  nnaordi  7698  nneob  7732  omsmolem  7733  erdisj  7794  qsss  7808  uniinqs  7827  map0g  7897  resixpfo  7946  ixpsnf1o  7948  xpdom3  8058  mapdom3  8132  phplem4  8142  php3  8146  unxpdomlem3  8166  ssfi  8180  findcard2  8200  findcard3  8203  frfi  8205  isfiniteg  8220  xpfi  8231  fiint  8237  finsschain  8273  dffi2  8329  marypha1lem  8339  marypha2  8345  supmo  8358  suplub2  8367  infmo  8401  ordiso2  8420  ordtypelem7  8429  ordtypelem8  8430  brwdom2  8478  unxpwdom2  8493  ixpiunwdom  8496  elirrv  8504  suc11reg  8516  noinfep  8557  cantnfle  8568  cantnflem1  8586  cantnf  8590  trcl  8604  epfrs  8607  rankpwi  8686  rankunb  8713  rankuni2b  8716  rankxplim3  8744  cplem1  8752  karden  8758  carddom2  8803  fseqenlem2  8848  ac10ct  8857  acni2  8869  acndom  8874  infpwfien  8885  alephordi  8897  alephord  8898  iunfictbso  8937  aceq3lem  8943  dfac5  8951  dfac2  8953  dfac12lem3  8967  dfac12r  8968  cdainflem  9013  cdainf  9014  cfub  9071  cfeq0  9078  coflim  9083  cfslb2n  9090  cofsmo  9091  coftr  9095  infpssr  9130  fin23lem7  9138  fin23lem11  9139  fin23lem21  9161  isf32lem2  9176  isf34lem4  9199  isfin1-2  9207  isfin1-3  9208  fin1a2lem9  9230  fin1a2lem11  9232  fin1a2lem12  9233  fin1a2lem13  9234  domtriomlem  9264  axdc3lem2  9273  axcclem  9279  ac6c4  9303  zorn2lem4  9321  zorn2lem5  9322  zorn2lem7  9324  ttukeylem5  9335  ttukeyg  9339  brdom6disj  9354  fnrndomg  9358  iunfo  9361  iundom2g  9362  ficard  9387  konigthlem  9390  alephval2  9394  pwcfsdom  9405  fpwwe2lem9  9460  fpwwe2lem11  9462  fpwwe2lem12  9463  fpwwe2lem13  9464  pwfseqlem3  9482  gchpwdom  9492  winalim2  9518  gchina  9521  wunex2  9560  tskr1om2  9590  tskxpss  9594  inar1  9597  tskuni  9605  gruun  9628  grudomon  9639  grur1  9642  ltmpi  9726  ltexprlem2  9859  ltexprlem6  9863  reclem2pr  9870  reclem3pr  9871  reclem4pr  9872  suplem1pr  9874  mulgt0sr  9926  supsrlem  9932  axrrecex  9984  axpre-sup  9990  ltlen  10138  addid0  10450  negn0  10459  negf1o  10460  mulge0b  10893  supaddc  10990  supadd  10991  supmul1  10992  supmullem1  10993  supmullem2  10994  supmul  10995  cju  11016  nnsub  11059  0mnnnnn0  11325  un0addcl  11326  un0mulcl  11327  nn0sub  11343  nn0n0n1ge2b  11359  peano5uzi  11466  eluzuzle  11696  zsupss  11777  qbtwnre  12030  xrsupexmnf  12135  xrinfmexpnf  12136  xrsupsslem  12137  xrinfmsslem  12138  xrub  12142  supxrun  12146  ixxdisj  12190  icodisj  12297  difreicc  12304  uzsubsubfz  12363  fzadd2  12376  elfzmlbp  12450  fzofzim  12514  elfznelfzo  12573  injresinj  12589  subfzo0  12590  flval3  12616  modirr  12741  modsumfzodifsn  12743  addmodlteq  12745  ssnn0fi  12784  seqf1o  12842  expcl2lem  12872  expnegz  12894  expaddz  12904  expmulz  12906  facwordi  13076  faclbnd4lem4  13083  bccl  13109  hashnfinnn0  13152  hashgt12el  13210  hashgt12el2  13211  hashfun  13224  hashbclem  13236  hashbc  13237  hashfacen  13238  hashf1lem1  13239  hashf1  13241  hash2pwpr  13258  fundmge2nop0  13274  fi1uzind  13279  brfi1indALT  13282  fi1uzindOLD  13285  brfi1indALTOLD  13288  wrdind  13476  wrd2ind  13477  reuccats1  13480  swrdccatin1  13483  swrdccatin2  13487  swrdccat3  13492  swrdccat3blem  13495  cshw1  13568  cshwcsh2id  13574  wwlktovfo  13701  s3iunsndisj  13707  rtrclreclem3  13800  dfrtrcl2  13802  sqrlem1  13983  sqrlem6  13988  rexanre  14086  cau3lem  14094  2clim  14303  summo  14448  fsum2dlem  14501  fsumiun  14553  prodmo  14666  fprod2dlem  14710  bpolycl  14783  rpnnen2lem12  14954  odd2np1lem  15064  oddge22np1  15073  sqoddm1div8z  15078  sumeven  15110  pwp1fsum  15114  bitsfzo  15157  sadcaddlem  15179  gcd0id  15240  algcvgblem  15290  lcmfunsnlem1  15350  lcmfunsnlem2lem1  15351  lcmfunsnlem2  15353  coprmproddvdslem  15376  divgcdcoprm0  15379  isprm7  15420  prmdvdsexpr  15429  prmfac1  15431  qnumdencl  15447  hashdvds  15480  prm23lt5  15519  pcneg  15578  prmpwdvds  15608  prmreclem2  15621  4sqlem12  15660  vdwlem6  15690  vdwlem10  15694  vdwlem13  15697  0ram  15724  ram0  15726  ramz  15729  ramcl  15733  prmgaplem3  15757  prmgaplem4  15758  prmgaplem5  15759  prmgaplem6  15760  cshwshashlem1  15802  prmlem0  15812  firest  16093  imasaddfnlem  16188  imasvscafn  16197  mremre  16264  cicsym  16464  initoid  16655  termoid  16656  iszeroi  16659  drsdirfi  16938  pospo  16973  joinfval  17001  meetfval  17015  lubun  17123  odupos  17135  acsfiindd  17177  psss  17214  mnd1id  17332  dfgrp2e  17448  dfgrp3lem  17513  symgfix2  17836  f1omvdco2  17868  symggen  17890  odcau  18019  pgpfi  18020  sylow2blem3  18037  sylow3lem2  18043  lsmmod  18088  efgsfo  18152  frgpuptinv  18184  frgpnabllem1  18276  cyggeninv  18285  lt6abl  18296  cyggex2  18298  gsumval3lem2  18307  gsumval3  18308  gsum2d2  18373  dmdprdd  18398  dprd2da  18441  pgpfac1lem5  18478  pgpfac  18483  srgbinomlem4  18543  dvdsrtr  18652  dvdsrmul1  18653  lss1d  18963  lspsolvlem  19142  lspsnat  19145  lbsextlem2  19159  lbsextlem3  19160  0ring  19270  01eq0ring  19272  0ring01eqbi  19273  rng1nfld  19278  domnmuln0  19298  abvn0b  19302  mvrf1  19425  mplcoe5lem  19467  opsrtoslem2  19485  cply1mul  19664  coe1fzgsumdlem  19671  gsummoncoe1  19674  pf1ind  19719  evl1gsumdlem  19720  xrsdsreclblem  19792  qsssubdrg  19805  prmirredlem  19841  cygznlem3  19918  obslbs  20074  dsmmacl  20085  lindfrn  20160  lmiclbs  20176  lmisfree  20181  matecl  20231  mat1dimelbas  20277  scmateALT  20318  mdetdiaglem  20404  mdet0  20412  mdetunilem9  20426  gsummatr01  20465  cpmatmcllem  20523  m2cpminvid2lem  20559  pmatcollpw3fi1lem2  20592  chfacfscmul0  20663  chfacfpmmul0  20667  cayhamlem3  20692  tgcl  20773  tgidm  20784  indistopon  20805  fctop  20808  cctop  20810  ppttop  20811  pptbas  20812  epttop  20813  opnnei  20924  neiptopnei  20936  tgrest  20963  restntr  20986  perfopn  20989  ordtrest2lem  21007  isreg2  21181  lmmo  21184  ordthauslem  21187  cmpsublem  21202  cmpsub  21203  cmpcld  21205  hauscmplem  21209  iunconnlem  21230  unconn  21232  2ndcrest  21257  2ndcctbss  21258  2ndcdisj  21259  dis2ndc  21263  locfincmp  21329  comppfsc  21335  txbas  21370  ptbasin  21380  ptbasfi  21384  txcls  21407  txbasval  21409  ptpjopn  21415  ptclsg  21418  dfac14lem  21420  xkoccn  21422  txcnp  21423  txindis  21437  txdis1cn  21438  tx1stc  21453  tx2ndc  21454  txkgen  21455  xkoco1cn  21460  xkoco2cn  21461  xkococn  21463  xkoinjcn  21490  txconn  21492  fbfinnfr  21645  opnfbas  21646  filtop  21659  isfild  21662  fbunfip  21673  filconn  21687  fbasrn  21688  filuni  21689  isufil2  21712  filssufilg  21715  ufileu  21723  filufint  21724  rnelfmlem  21756  rnelfm  21757  fmfnfmlem2  21759  fmfnfmlem4  21761  fmfnfm  21762  hausflimi  21784  hauspwpwf1  21791  flffbas  21799  flftg  21800  alexsublem  21848  alexsubALTlem1  21851  alexsubALTlem2  21852  alexsubALTlem3  21853  alexsubALTlem4  21854  alexsubALT  21855  ptcmplem3  21858  cldsubg  21914  qustgpopn  21923  tgptsmscld  21954  tsmsxplem1  21956  ustfilxp  22016  imasdsf1olem  22178  bldisj  22203  xbln0  22219  prdsxmslem2  22334  xrsblre  22614  icccmplem2  22626  reconn  22631  opnreen  22634  xrge0tsms  22637  metdsre  22656  iccpnfcnv  22743  cnheiborlem  22753  phtpc01  22796  pi1blem  22839  tchcph  23036  cfilfcls  23072  iscau4  23077  bcthlem5  23125  bcth3  23128  hlhil  23214  ovolctb  23258  ovoliunlem2  23271  ovoliunnul  23275  ovolicc2  23290  volfiniun  23315  iundisj  23316  dyadmax  23366  dyadmbllem  23367  vitalilem2  23378  ismbfd  23407  mbfimaopnlem  23422  itg11  23458  i1faddlem  23460  mbfi1fseqlem4  23485  bddmulibl  23605  limciun  23658  perfdvf  23667  rolle  23753  dvivthlem1  23771  dvne0  23774  lhop1  23777  lhop2  23778  itgsubst  23812  dvdsq1p  23920  fta1g  23927  dgrco  24031  plydivex  24052  fta1  24063  ulmcaulem  24148  abelthlem2  24186  pilem2  24206  cxpmul2z  24437  cxpcn3lem  24488  xrlimcnp  24695  jensen  24715  wilthlem2  24795  wilthlem3  24796  muval2  24860  sqf11  24865  ppiublem1  24927  fsumvma  24938  lgsdir2lem2  25051  lgsdir2lem5  25054  lgsqrmodndvds  25078  gausslemma2dlem1a  25090  gausslemma2dlem3  25093  gausslemma2d  25099  2lgsoddprmlem2  25134  dchrisum0fno1  25200  pntlem3  25298  pntleml  25300  ostthlem1  25316  ostth2lem2  25323  colinearalg  25790  axcontlem2  25845  axcontlem8  25851  edgupgr  26029  umgrpredgv  26035  numedglnl  26039  ausgrumgri  26062  ausgrusgri  26063  ushgredgedg  26121  ushgredgedgloop  26123  uhgr0v0e  26130  subumgredg2  26177  uhgrspansubgrlem  26182  uhgrspan1  26195  upgrreslem  26196  umgrreslem  26197  upgrres1  26205  fusgrfisstep  26221  nbuhgr  26239  nbuhgr2vtx1edgb  26248  uhgrnbgr0nb  26250  edgnbusgreu  26269  nbusgredgeu0  26270  nbusgrf1o0  26271  nbusgrvtxm1uvtx  26306  cusgredg  26320  cusgrfi  26354  usgredgsscusgredg  26355  1loopgrnb0  26398  usgrvd0nedg  26429  uhgrvd00  26430  upgriswlk  26537  upgrwlkcompim  26539  uspgr2wlkeq  26542  uspgr2wlkeqi  26544  wlkv0  26547  wlklenvclwlk  26551  wlkp1lem6  26575  lfgrwlkprop  26584  spthdep  26630  upgrwlkdvdelem  26632  usgr2wlkneq  26652  usgr2trlncl  26656  pthdlem1  26662  pthdlem2lem  26663  clwlkl1loop  26678  crctcshwlkn0lem3  26704  crctcshwlkn0lem5  26706  crctcshwlkn0  26713  0enwwlksnge1  26749  wlkiswwlks2  26761  wlkiswwlksupgr2  26763  wlkwwlksur  26783  umgr2adedgspth  26844  wwlks2onv  26847  clwlkclwwlklem2a4  26898  clwlkclwwlklem2  26901  clwwlksf1  26917  erclwwlkstr  26936  erclwwlksntr  26948  hashecclwwlksn1  26954  umgrhashecclwwlk  26955  clwlksfoclwwlk  26963  eucrctshift  27103  3cyclfrgrrn1  27149  frgrnbnb  27157  frgrncvvdeqlem2  27164  frgrncvvdeqlem3  27165  frgrncvvdeqlem9  27171  frgrwopregbsn  27181  frgrwopreg1  27182  frgrwopreg2  27183  frgrwopreglem5lem  27184  frgrwopreglem5ALT  27186  numclwlk1lem2f1  27227  lnon0  27653  shmodsi  28248  shlub  28273  spanunsni  28438  h1datomi  28440  stm1ri  29103  stadd3i  29107  mdsl1i  29180  cvmdi  29183  superpos  29213  chjatom  29216  chirredi  29253  atcvat4i  29256  sumdmdii  29274  sumdmdlem  29277  cdj3lem2a  29295  cdj3lem3a  29298  cdj3i  29300  disji2f  29390  disjif2  29394  iundisjf  29402  rnmpt2ss  29473  iundisjfi  29555  nn0min  29567  xrge0tsmsd  29785  cnre2csqima  29957  ordtrest2NEWlem  29968  xrge0iifcnv  29979  lmxrge0  29998  measdivcstOLD  30287  dya2iocuni  30345  omssubadd  30362  eulerpartlems  30422  bnj849  30995  bnj1118  31052  derangenlem  31153  erdszelem9  31181  pconnconn  31213  iccllysconn  31232  cvmsval  31248  cvmscld  31255  cvmsss2  31256  cvmopnlem  31260  cvmfolem  31261  cvmliftmolem2  31264  cvmlift2lem10  31294  cvmlift2lem12  31296  cvmlift3lem5  31305  cvmlift3lem8  31308  msubvrs  31457  mthmblem  31477  untsucf  31587  3orel2  31592  3orel3  31593  nepss  31599  eqfunresadj  31659  dfon2lem5  31692  dfon2lem6  31693  dfon2lem7  31694  dfon2lem8  31695  rdgprc  31700  trpredtr  31730  dftrpred3g  31733  trpredrec  31738  frmin  31739  frind  31740  frins2fg  31744  wzel  31771  wsuclem  31773  wsuclemOLD  31774  frrlem5e  31788  nosepon  31818  noextendseq  31820  nolesgn2ores  31825  nosepdmlem  31833  nodenselem8  31841  noetalem3  31865  nocvxmin  31894  scutun12  31917  funpartfun  32050  altopth1  32072  altopth2  32073  colineardim1  32168  lineext  32183  btwnconn1lem14  32207  brsegle  32215  hilbert1.2  32262  trer  32310  elicc3  32311  finminlem  32312  fneint  32343  fnessref  32352  refssfne  32353  neibastop1  32354  neibastop2lem  32355  neibastop2  32356  fnemeet2  32362  fnejoin2  32364  tailfb  32372  arg-ax  32415  ordtoplem  32434  onsuct0  32440  bj-gl4lem  32579  bj-sngltag  32971  bj-restn0  33043  bj-0int  33055  bj-ismooredr2  33065  bj-bary1lem1  33161  icorempt2  33199  icoreresf  33200  relowlssretop  33211  finxpreclem6  33233  wl-ax8clv2  33381  fin2so  33396  poimirlem24  33433  poimirlem25  33434  poimirlem26  33435  poimirlem27  33436  poimirlem29  33438  poimirlem30  33439  poimirlem31  33440  mblfinlem1  33446  mblfinlem4  33449  ovoliunnfl  33451  itg2addnclem  33461  itg2addnclem2  33462  areacirc  33505  unirep  33507  filbcmb  33535  sdclem1  33539  fdc  33541  nninfnub  33547  isbnd2  33582  ssbnd  33587  prdsbnd2  33594  cntotbnd  33595  heibor1lem  33608  heiborlem1  33610  heiborlem4  33613  heiborlem6  33615  0idl  33824  intidl  33828  unichnidl  33830  keridl  33831  prnc  33866  iss2  34112  prtlem17  34161  prter2  34166  ax12indn  34228  lsatn0  34286  lsatcmp  34290  lssat  34303  lfl1  34357  lshpsmreu  34396  lkrin  34451  glbconxN  34664  cvrat4  34729  paddasslem17  35122  pmodlem2  35133  dalawlem14  35170  pclclN  35177  pclfinN  35186  pclfinclN  35236  poml4N  35239  osumcllem8N  35249  pexmidlem5N  35260  cdleme32a  35729  cdlemg33b0  35989  tendoeq2  36062  diaelrnN  36334  dihmeetlem1N  36579  dihglblem5apreN  36580  dihglblem2N  36583  dochvalr  36646  dochkrshp  36675  lcfl6  36789  lcfrvalsnN  36830  mapdordlem2  36926  mapdh8b  37069  mapdh9a  37079  hdmap14lem13  37172  eldioph2b  37326  eldiophss  37338  diophren  37377  ctbnfien  37382  rencldnfilem  37384  pellexlem3  37395  pellexlem5  37397  pellex  37399  pell14qrexpcl  37431  pellfundre  37445  pellfundge  37446  pellfundlb  37448  pellfundglb  37449  jm2.19lem4  37559  fnwe2lem2  37621  pwssplit4  37659  hbtlem5  37698  ss2iundf  37951  relexpmulg  38002  relexpxpmin  38009  relexpaddss  38010  dftrcl3  38012  dfrtrcl3  38025  clsk1indlem3  38341  isotone1  38346  isotone2  38347  ntrneiel2  38384  ntrneik4w  38398  onfrALT  38764  ax6e2ndeq  38775  snssiALT  39063  iinssf  39327  hirstL-ax3  41059  2reurex  41181  otiunsndisjX  41298  subsubelfzo0  41336  iccpartiltu  41358  iccpartigtl  41359  iccpartltu  41361  pfxccat3  41426  pfxccat3a  41429  reuccatpfxs1  41434  fmtnofac2lem  41480  fmtno4prmfac  41484  prmdvdsfmtnof1lem1  41496  lighneallem2  41523  opoeALTV  41594  opeoALTV  41595  even3prm2  41628  gbegt5  41649  gbowgt5  41650  sbgoldbwt  41665  sbgoldbst  41666  sbgoldbalt  41669  sbgoldbm  41672  mogoldbb  41673  sbgoldbo  41675  nnsum3primesle9  41682  nnsum4primeseven  41688  nnsum4primesevenALTV  41689  wtgoldbnnsum4prm  41690  bgoldbnnsum3prm  41692  bgoldbtbndlem1  41693  bgoldbtbndlem4  41696  bgoldbtbnd  41697  upgrwlkupwlk  41721  sprsymrelf1lem  41741  sprsymrelfolem2  41743  sprsymrelf1  41746  sprsymrelfo  41747  mgmpropd  41775  copisnmnd  41809  mgm2mgm  41863  ringrng  41879  c0snmgmhm  41914  ztprmneprm  42125  mndpsuppss  42152  lindslinindimp2lem4  42250  lindslinindsimp2  42252  lindsrng01  42257  snlindsntor  42260  ldepspr  42262  isldepslvec2  42274  suppdm  42300  blen1b  42382  dignn0ldlem  42396  digexp  42401  nn0sumshdiglemB  42414  nn0sumshdiglem1  42415  iunord  42422  tfis2d  42427