Theorem syl6ibr 229

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

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

This theorem is referenced by:  imp4a 389  pm5.18 719  nic-ax 1086  3impexpbicom 1129  hband 1307  equs5e 1405  euim 1654  mopick2 1674  mopick2OLD 1675  euor2OLD 1677  2moswap 1685  2eu1 1690  necon3ad 1872  necon3bdOLD 1875  necon3d 1876  necon2adOLD 1891  necon1d 1917  r19.21ad 2014  cla4egf 2195  cla42gv 2200  cla43gv 2202  eqsbc3r 2340  ra5 2372  tpid3g 2937  difsnOLD 2948  pwpw0 2956  sssn 2964  pwsnALT 2995  ssuniOLD 3024  ssiun 3114  ssiun2 3116  wefrc 3467  tron 3496  ordtri3or 3506  ordtri3orOLD 3507  ordtri3OLD 3513  oneqmini 3529  dfwe2OLD 3673  ssorduniOLD 3682  tfis 3749  nnsuc 3780  ssrelOLD 3887  ssrelrelOLD 3895  opeldm 3971  dmcosseq 4025  relssres 4059  cotrOLD 4114  cnvsymOLD 4116  ssrnres 4165  funssOLD 4251  fnun 4331  f1oun 4469  nfunsnOLD 4518  ssimaex 4540  fvopab3ig 4552  chfnrn 4586  dffo4 4604  dffo5 4605  fvclss 4642  isomin 4687  isofrlem 4689  f1oweALT 4694  fnoprabg 4752  oprabvalig 4764  rdglim2 4968  tz7.48lem 4975  tz7.49 4979  domtriord 5357  infsdomnn 5435  pssnn 5438  ssfi 5440  pm54.43 5472  ordtypelem4 5497  ordtypelem7 5500  onsdom 5504  inf3lem4 5531  rankr1 5594  r1pwcl 5607  19.21a3con13v 5637  omsubsuc2 5674  elomsubsd 5681  aceq5lem4 5696  aceq5 5698  aceq6b 5700  ac5b 5711  kmlem2 5724  zorn2lem4 5749  zorn2lem6 5751  zorn2lem7 5752  cardne 5776  carden 5777  carddom 5783  alephordi 5818  cardaleph 5829  carduniima 5834  cardinfima 5835  alephval3 5847  cflim 5853  indpi 5982  ltaddpq 6027  genpcl 6059  prlem934 6087  ltaddpr 6088  ltexprlem1 6090  ltexprlem5 6094  reclem4pr 6107  suplem1pr 6109  pre-axsup 6240  zaddcl 7169  zmulcl 7184  zneo 7207  uzwo4OLD 7217  icoshft 7372  uzwo 7419  uzwoOLD 7420  sqr2irr 7774  caubndi 7973  bccl2 8018  iserzcmp0 8198  caucvglem2 8213  basgen2 8704  distop 8714  cnpco 8841  cncnplem2 8847  metreslem 8894  unirnbl 8947  metelcls 9038  ssga 9250  gapmlem 9256  gapm 9257  ubthlem5 9671  oprabvaligg 9948  findcard 9970  findcardOLD 9971  cdrci 9975  uptx 10018  subtopmetlem 10047  subtopmet 10048  fipfil 10063  fipfil2 10064  filintf 10066  fbunfip 10074  filrn 10085  shmodsi 10787  orthin 10795  h1datomi 10929  osumlem4 11008  stcltr2i 11639  atom1d 11717  sumdmdii 11779  cdj3lem1 11798  bnj599 12352  bnj1168 12752  bnj1169 12753  bnj1016 13168  negn0 13447  dvds2lem 13459  dvdslelem 13484  divalglem8 13495  prmdvdsmul 13576  truni 13584  trsuc2 13585  fundmpss 13629  tfisg 13704  wfisg 13709  frinsg 13733  frxp 13743  poseq 13746  sltval2 13789  axdenselem7 13815  inttr 14107  restidsing 14121  repcpwti 14229  nZdef 14253  inttop2 14586  fbaslim2 14650  rdmob 14777  isline1 14976  dmsdtriordOLD 15042  ordtypelem4OLD 15060  ordtypelem7OLD 15063  onsdomOLD 15067  omsubsuc2OLD 15069  elomsubsdOLD 15076  compsublem 15112  cptclsscpt 15114  hscptsscld 15116  compfipin0 15118  alexsublem3 15121  alexsub 15123  reconnlem4 15131  reconnlem5 15132  ivthALT 15136  fnessref 15185  locfincomp 15196  ist1-3 15225  isufil2 15247  filssufillem 15252  ufinffr 15260  ufilen 15261  filcon 15262  ufcondr 15263  fmfnfm 15280  fcluscomp 15303  tailfb 15321  filnetlem5 15326  cover2 15355  findcard2 15427  frfi 15453  uzm1 15466  sdc 15493  fdc 15494  totbndss 15619  heiborlem23 15659  heiborlem28 15664  recms 15692  abl4pnp 15719  phtpcdm 15743  isdivrng3 15794  crnghomfo 15836  intidl 15859  prtlem90 15928  prtlem10 15947  prtlem16 15954  prter2 15967  smores 16128  trsspwALT2 16300  trsspwALT3 16301  pwtr 16306  hlrelat 16792  pmaple 16967  pmapsub 16971

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 163

Copyright terms: Public domain