Theorem syl6ibr 255

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

Hypotheses

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

Assertion

Ref	Expression
syl6ibr	⊢ (𝜑 → (𝜓 → 𝜃))

Proof of Theorem syl6ibr

Step	Hyp	Ref	Expression
1		syl6ibr.1	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
2		syl6ibr.2	. . 3 ⊢ (𝜃 ↔ 𝜒)
3	2	biimpri 231	. 2 ⊢ (𝜒 → 𝜃)
4	1, 3	syl6 35	1 ⊢ (𝜑 → (𝜓 → 𝜃))

Syntax hints:   → wi 4   ↔ wb 209

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 210

This theorem is referenced by:  3imtr4g  299  nic-ax  1681  sbequ1  2247  dfmoeu  2535  2moswapv  2630  mopick2  2638  2moswap  2645  2eu6  2657  necon3d  2953  necon1d  2954  ralrimd  3129  spcimegf  3495  spcegf  3497  spcimedv  3500  spc2gv  3505  spc3gv  3509  rspcimedv  3518  2reu1  3796  pwpw0  4712  sssn  4725  pwsnOLD  4798  ssiun  4941  ssiun2  4942  wefrc  5530  ssrel  5639  dmcosseq  5827  relssres  5877  trin2  5968  ssrnres  6021  sossfld  6029  reuop  6136  frpoinsg  6175  wfisg  6183  tron  6214  ordtri3or  6223  oneqmini  6242  fnun  6468  f1oun  6658  brprcneu  6686  fvprc  6687  ssimaex  6774  chfnrn  6847  dffo4  6900  dffo5  6901  tpres  6994  fvclss  7033  isomin  7124  isofrlem  7127  isoselem  7128  fnoprabg  7311  nnsuc  7640  f1oweALT  7723  releldmdifi  7794  bropopvvv  7836  bropfvvvvlem  7837  frxp  7871  poxp  7873  fnse  7878  mpoxopynvov0g  7934  issmo2  8064  smores  8067  smogt  8082  rdglim2  8146  tz7.48lem  8155  tz7.49  8159  swoer  8399  qsss  8438  domtriord  8770  findcard  8819  findcard2  8820  pssnn  8824  pssnnOLD  8872  ssfiOLD  8873  findcard2OLD  8891  findcard3  8892  frfi  8894  dffi3  9025  supmo  9046  infmo  9089  inf3lem4  9224  carddom2  9558  fidomtri2  9575  pm54.43  9582  infpwfien  9641  alephordi  9653  cardaleph  9668  carduniima  9675  cardinfima  9676  alephval3  9689  dfac5lem4  9705  dfac5  9707  dfac2b  9709  kmlem2  9730  cflm  9829  cfslb2n  9847  cfsmolem  9849  isf32lem9  9940  axcc4  10018  domtriomlem  10021  zorn2lem4  10078  zorn2lem6  10080  fpwwe2lem10  10219  fpwwe2lem11  10220  inttsk  10353  inar1  10354  intgru  10393  ingru  10394  indpi  10486  nqpr  10593  ltaddpr  10613  ltexprlem1  10615  ltexprlem5  10619  reclem2pr  10627  reclem4pr  10629  negn0  11226  zmulcl  12191  uzm1  12437  uzwo  12472  xmullem2  12820  icoshft  13026  difreicc  13037  fzouzsplit  13242  ssfzoulel  13301  seqf1olem1  13580  seqf1olem2  13581  hashge2el2difr  14012  hashtpg  14016  reusq0  14991  modfsummod  15321  incexclem  15363  sqrt2irr  15773  dvds2lem  15793  dvdslelem  15833  oddnn02np1  15872  divalglem8  15924  dfgcd2  16069  2mulprm  16213  ge2nprmge4  16221  euclemma  16233  iserodd  16351  ramcl  16545  setsstruct  16705  mreiincl  17053  joinfval  17833  meetfval  17847  dirge  18063  sylow2alem1  18960  efgredlemb  19090  kerf1ghm  19717  rmodislmodlem  19920  lbspss  20073  lspsneu  20114  lspsnat  20136  lspsncv0  20137  opsrtoslem2  20967  distop  21846  epttop  21860  isclo2  21939  restdis  22029  subbascn  22105  cnrest2  22137  cnpresti  22139  isnrm2  22209  cmpsublem  22250  cmpcld  22253  dfconn2  22270  t1connperf  22287  1stcrest  22304  lly1stc  22347  uptx  22476  txcn  22477  prdstopn  22479  txconn  22540  cmphaushmeo  22651  fbasrn  22735  csdfil  22745  trufil  22761  fclscf  22876  alexsubALTlem3  22900  alexsubALT  22902  haustsms2  22988  ovoliunlem1  24353  ovoliunnul  24358  volsup2  24456  coeaddlem  25097  plymul0or  25128  radcnv0  25262  wilthlem3  25906  chtub  26047  gausslemma2dlem1a  26200  2sqlem10  26263  pntpbnd1  26421  mptelee  26940  axeuclidlem  27007  axcontlem4  27012  elntg2  27030  uhgrissubgr  27317  finsumvtxdg2size  27592  wlkonl1iedg  27707  pthdivtx  27770  wlkiswwlksupgr2  27915  eucrct2eupth  28282  isch3  29276  shmodsi  29424  orthin  29481  h1datomi  29616  stcltr2i  30310  atom1d  30388  sumdmdii  30450  cdj3lem1  30469  disjpreima  30596  lmxrge0  31570  dmvlsiga  31763  sibfof  31973  bnj600  32566  bnj1018g  32610  bnj1018  32611  bnj1173  32649  bnj1174  32650  pthisspthorcycl  32757  subgrwlk  32761  cusgracyclt3v  32785  erdszelem9  32828  cvmlift2lem1  32931  satfvsucsuc  32994  sat1el2xp  33008  fmla0xp  33012  fundmpss  33410  tfisg  33456  frinsg  33462  poseq  33482  sltval2  33545  noetalem1  33630  bday1s  33711  outsideofrflx  34115  nn0prpwlem  34197  ivthALT  34210  fnessref  34232  neibastop2lem  34235  tailfb  34252  bj-axtd  34462  bj-nfimt  34505  bj-nfdt0  34563  bj-nnfand  34617  bj-sbievw2  34716  bj-2upleq  34888  bj-restn0  34945  icorempo  35208  isbasisrelowllem2  35213  rdgellim  35233  rdgssun  35235  pibt2  35274  wl-lem-moexsb  35409  matunitlindflem1  35459  poimirlem3  35466  poimirlem4  35467  poimirlem29  35492  mblfinlem3  35502  itg2addnclem3  35516  cover2  35558  fdc  35589  nninfnub  35595  equivtotbnd  35622  prdstotbnd  35638  cntotbnd  35640  ablo4pnp  35724  isdrngo3  35803  crngohomfo  35850  intidl  35873  or32dd  35938  iss2  36165  prtlem18  36577  prter2  36581  lsat0cv  36733  lfl1  36770  lkreqN  36870  atlrelat1  37021  pmaple  37461  pmapsub  37468  pclclN  37591  pclfinN  37600  osumcllem4N  37659  pexmidlem1N  37670  cdleme7ga  37948  lcfl7N  39201  isdomn4  39835  rtprmirr  39996  ss2iundf  40885  brtrclfv2  40953  ismnushort  41533  nzss  41549  3impexpbicom  41713  alrim3con13v  41767  tratrb  41770  onfrALTlem3  41778  onfrALTlem2  41780  onfrALTlem1  41782  trsspwALT2  42053  trsspwALT3  42054  or2expropbi  44143  afv2orxorb  44335  lswn0  44512  ich2exprop  44539  prproropf1olem4  44574  paireqne  44579  reupr  44590  lighneallem4b  44677  sbgoldbwt  44845  sbgoldbst  44846  sbgoldbalt  44849  isomuspgrlem1  44895  isomuspgrlem2d  44899  isupwlkg  44915  2zrngamgm  45113  fldivexpfllog2  45527  line2ylem  45713  fdomne0  45793