Theorem syl6ibr 242

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	|- ( ph -> ( ps -> ch ) )
syl6ibr.2	|- ( th <-> ch )

Assertion

Ref	Expression
syl6ibr	|- ( ph -> ( ps -> th ) )

Proof of Theorem syl6ibr

Step	Hyp	Ref	Expression
1		syl6ibr.1	. 2 |- ( ph -> ( ps -> ch ) )
2		syl6ibr.2	. . 3 |- ( th <-> ch )
3	2	biimpri 218	. 2 |- ( ch -> th )
4	1, 3	syl6 35	1 |- ( ph -> ( ps -> th ) )

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  imp4aOLD  615  nic-ax  1598  nfimt  1821  nfimdOLD  2226  mo2v  2477  euim  2523  mopick2  2540  2moswap  2547  2eu6  2558  necon3d  2815  necon1d  2816  ralrimd  2959  spcimegf  3287  spcegf  3289  spcimedv  3292  spc2gv  3296  spc3gv  3298  rspcimedv  3311  eqsbc3rOLD  3493  tpid3gOLD  4306  pwpw0  4344  sssn  4358  pwsnALT  4429  ssiun  4562  ssiun2  4563  wefrc  5108  ssrel  5207  dmcosseq  5387  relssres  5437  restidsingOLD  5459  trin2  5519  ssrnres  5572  sossfld  5580  wfisg  5715  tron  5746  ordtri3or  5755  oneqmini  5776  fnun  5997  f1oun  6156  brprcneu  6184  ssimaex  6263  chfnrn  6328  dffo4  6375  dffo5  6376  tpres  6466  fvclss  6500  isomin  6587  isofrlem  6590  isoselem  6591  fnoprabg  6761  nnsuc  7082  f1oweALT  7152  bropopvvv  7255  bropfvvvvlem  7256  frxp  7287  poxp  7289  fnse  7294  mpt2xopynvov0g  7340  issmo2  7446  smores  7449  smogt  7464  rdglim2  7528  tz7.48lem  7536  tz7.49  7540  swoer  7772  qsss  7808  domtriord  8106  pssnn  8178  ssfi  8180  findcard  8199  findcard2  8200  findcard3  8203  frfi  8205  dffi3  8337  supmo  8358  infmo  8401  inf3lem4  8528  carddom2  8803  fidomtri2  8820  pm54.43  8826  infpwfien  8885  alephordi  8897  cardaleph  8912  carduniima  8919  cardinfima  8920  alephval3  8933  dfac5lem4  8949  dfac5  8951  dfac2  8953  kmlem2  8973  cflm  9072  cfslb2n  9090  cfsmolem  9092  isf32lem9  9183  axcc4  9261  domtriomlem  9264  zorn2lem4  9321  zorn2lem6  9323  fpwwe2lem11  9462  fpwwe2lem12  9463  inttsk  9596  inar1  9597  intgru  9636  ingru  9637  indpi  9729  nqpr  9836  ltaddpr  9856  ltexprlem1  9858  ltexprlem5  9862  reclem2pr  9870  reclem4pr  9872  negn0  10459  zmulcl  11426  uzm1  11718  uzwo  11751  xmullem2  12095  icoshft  12294  difreicc  12304  fzouzsplit  12503  ssfzoulel  12562  seqf1olem1  12840  seqf1olem2  12841  hashge2el2difr  13263  hashtpg  13267  swrdccatin2  13487  modfsummod  14526  incexclem  14568  sqrt2irr  14979  dvds2lem  14994  dvdslelem  15031  oddnn02np1  15072  divalglem8  15123  dfgcd2  15263  euclemma  15425  iserodd  15540  ramcl  15733  setsstruct  15898  mreiincl  16256  joinfval  17001  meetfval  17015  dirge  17237  sylow2alem1  18032  efgredlemb  18159  kerf1hrm  18743  rmodislmodlem  18930  lbspss  19082  lspsneu  19123  lspsnat  19145  lspsncv0  19146  opsrtoslem2  19485  distop  20799  epttop  20813  isclo2  20892  restdis  20982  subbascn  21058  cnrest2  21090  cnpresti  21092  isnrm2  21162  cmpsublem  21202  cmpcld  21205  dfconn2  21222  t1connperf  21239  1stcrest  21256  lly1stc  21299  uptx  21428  txcn  21429  prdstopn  21431  txconn  21492  cmphaushmeo  21603  fbasrn  21688  csdfil  21698  trufil  21714  fclscf  21829  alexsubALTlem3  21853  alexsubALT  21855  haustsms2  21940  ovoliunlem1  23270  ovoliunnul  23275  volsup2  23373  coeaddlem  24005  plymul0or  24036  radcnv0  24170  wilthlem3  24796  chtub  24937  gausslemma2dlem1a  25090  2sqlem10  25153  pntpbnd1  25275  mptelee  25775  axeuclidlem  25842  axcontlem4  25847  uhgrissubgr  26167  nbgrnself2  26259  finsumvtxdg2size  26446  wlkonl1iedg  26561  pthdivtx  26625  wlkiswwlksupgr2  26763  eucrct2eupth  27105  isch3  28098  shmodsi  28248  orthin  28305  h1datomi  28440  stcltr2i  29134  atom1d  29212  sumdmdii  29274  cdj3lem1  29293  disjpreima  29397  lmxrge0  29998  dmvlsiga  30192  sibfof  30402  bnj600  30989  bnj1018  31032  bnj1173  31070  bnj1174  31071  erdszelem9  31181  cvmlift2lem1  31284  fundmpss  31664  tfisg  31716  frinsg  31742  poseq  31750  sltval2  31809  outsideofrflx  32234  nn0prpwlem  32317  ivthALT  32330  fnessref  32352  neibastop2lem  32355  tailfb  32372  bj-axtd  32578  bj-ssbequ1  32644  bj-nfdt0  32685  bj-2upleq  33000  bj-restn0  33043  icorempt2  33199  isbasisrelowllem2  33204  wl-ax8clv2  33381  matunitlindflem1  33405  poimirlem3  33412  poimirlem4  33413  poimirlem29  33438  mblfinlem3  33448  itg2addnclem3  33463  cover2  33508  fdc  33541  nninfnub  33547  equivtotbnd  33577  prdstotbnd  33593  cntotbnd  33595  ablo4pnp  33679  isdrngo3  33758  crngohomfo  33805  intidl  33828  or32dd  33896  iss2  34112  prtlem18  34162  prter2  34166  lsat0cv  34320  lfl1  34357  lkreqN  34457  atlrelat1  34608  pmaple  35047  pmapsub  35054  pclclN  35177  pclfinN  35186  osumcllem4N  35245  pexmidlem1N  35256  cdleme7ga  35535  lcfl7N  36790  ss2iundf  37951  brtrclfv2  38019  nzss  38516  3impexpbicom  38685  alrim3con13v  38743  tratrb  38746  onfrALTlem3  38759  onfrALTlem2  38761  onfrALTlem1  38763  trsspwALT2  39046  trsspwALT3  39047  2reu1  41186  lswn0  41380  lighneallem4b  41526  sbgoldbwt  41665  sbgoldbst  41666  sbgoldbalt  41669  isupwlkg  41718  2zrngamgm  41939  fldivexpfllog2  42359