Theorem syl6ibr 211

Description: A mixed syllogism inference from a nested implication and a biconditional. Useful for substituting an embedded consequent with a definition.

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 150	. 2 |- (ch -> th)
4	1, 3	syl6 22	1 |- (ph -> (ps -> th))

Syntax hints:   -> wi 3   <-> wb 144

This theorem is referenced by:  imp4a 362  nic-ax 969  hband 1147  equs5e 1235  mopick2 1476  euor2 1477  2moswap 1484  2eu1 1489  necon3bd 1646  necon3d 1647  necon2ad 1657  r19.21ad 1763  cla4egf 1907  cla42gv 1911  cla43gv 1913  ra5 2050  difsn 2528  pwpw0 2533  sssn 2538  pwsnALT 2566  ssuni 2589  wefrc 2970  tron 2998  ordtri3or 3007  ordtri3 3011  oneqmini 3024  dfwe2 3140  ssorduni 3147  tfis 3208  nnsuc 3235  ssrel 3334  ssrelrel 3340  opeldm 3405  relssres 3482  cotr 3528  cnvsym 3529  ssrnres 3566  funss 3639  fnun 3700  f1oun 3815  ssimaex 3879  fvopab3ig 3889  chfnrn 3916  dffo4 3934  dffo5 3935  fvclss 3969  isomin 4013  isofrlem 4015  f1oweALT 4020  fnoprabg 4072  oprabvalig 4084  rdglim2 4250  tz7.48lem 4256  tz7.49 4260  infsdomnn 4678  pssnn 4681  ssfi 4683  pm54.43 4715  inf3lem4 4761  rankr1 4820  r1pwcl 4833  aceq5lem4 4884  aceq5 4886  aceq6b 4888  ac5b 4899  kmlem2 4912  zorn2lem4 4937  zorn2lem6 4939  zorn2lem7 4940  cardne 4978  carden 4979  carddom 4985  alephordi 5024  cardaleph 5035  carduniima 5040  cardinfima 5041  alephval3 5053  cflim 5059  indpi 5188  ltaddpq 5233  genpcl 5265  prlem934 5293  ltaddpr 5294  ltexprlem1 5296  ltexprlem5 5300  reclem4pr 5313  suplem1pr 5315  pre-axsup 5445  zaddcl 6333  zmulcl 6348  zneo 6371  uzwo4OLD 6381  icoshft 6535  uzwo 6582  uzwoOLD 6583  nn0opthi 6867  sqr2irr 6930  caubndi 7129  bccl2 7174  iserzcmp0 7346  caucvglem2 7361  basgen2 7851  distop 7861  cnpco 7979  cncnplem2 7985  metreslem 8032  unirnbl 8085  metelcls 8176  ubthlem5 8791  shmodsi 9638  orthin 9646  h1datomi 9780  osumlem4 9859  stcltr2i 10483  atom1d 10561  sumdmdii 10624  cdj3lem1 10643  oprabvaligg 10729  inttr 10787  restidsing 10805  cdrci 10994  fipfil 11076  fipfil2 11077  filintf 11081  rdmob 11202  dmsdtriord 11408  ordtypelem4 11430  ordtypelem7 11433  onsdom 11437  omsubsuc2 11439  elomsubsd 11446  compsublem 11487  cptclsscpt 11489  hscptsscld 11491  compfipin0 11493  alexsublem3 11498  alexsub 11500  subtopmetlem 11505  subtopmet 11506  reconnlem4 11510  reconnlem5 11511  ivthALT 11515  fnessref 11564  locfincomp 11575  ist1-3 11604  fbunfip 11631  filrn 11643  isufil2 11650  filssufillem 11655  ufinffr 11663  ufilen 11664  filcon 11665  ufcondr 11666  fmfnfm 11704  fcluscomp 11733  tailfb 11762  filnetlem5 11767  ssga 11777  gapmlem 11783  gapm 11784  findcard 11836  uzm1 11862  sdc 11877  metsstop 11909  uptx 11978  totbndss 11993  heiborlem23 12033  heiborlem28 12038  recms 12066  phtpcdm 12103

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7

This theorem depends on definitions:  df-bi 145

Copyright terms: Public domain