Theorem syl6ib 229

Description: A mixed syllogism inference from a nested implication and a biconditional.

Hypotheses

Ref	Expression
syl6ib.1	|- (ph -> (ps -> ch))
syl6ib.2	|- (ch <-> th)

Assertion

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

Proof of Theorem syl6ib

Step	Hyp	Ref	Expression
1		syl6ib.1	. 2 |- (ph -> (ps -> ch))
2		syl6ib.2	. . 3 |- (ch <-> th)
3	2	biimpi 168	. 2 |- (ch -> th)
4	1, 3	syl6 25	1 |- (ph -> (ps -> th))

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

This theorem is referenced by:  pm3.37 308  exp4a 409  pm5.18OLD 723  19.23 1411  19.29OLD 1422  cbvexd 1704  ax15 1750  2eu3 1855  exists2 1863  necon2bd 2057  necon2d 2058  necon4ad 2071  necon4bdOLD 2074  necon4d 2075  necon4dOLD 2076  necon1bd 2080  eqsbc3r 2507  ssralv2 2674  reupick 2874  sspr 3144  trin 3422  pwssun 3578  efrirr 3637  wefrc 3652  ordtri3 3697  onfr 3702  suc11 3773  onmindif2 3893  ssrelOLD 4076  ssrelrelOLD 4084  elreldm 4185  issOLD 4255  xp11 4347  ssrnres 4354  opelf 4579  dffo4 4793  mapsn 5404  en2d 5459  domtriord 5546  nneneq 5606  unblem1 5633  supnub 5672  onsdom 5694  suc11reg 5710  inf3lem2 5720  trcl 5752  en3lplem2 5757  tz9.13 5774  tratrb 5831  truniALT 5845  aceq5lem5 5901  entric 5990  unxpdomlem 5995  carduniima 6038  cardinfima 6039  alephval2 6050  distrlem2pr 6280  ltapr 6303  suppsrlem 6373  suppsr2 6375  suprelem 6411  ssxrOLD 6715  ngtmnft 6742  sup2 7260  nnunb 7279  elnn0nn 7380  nneoi 7409  uzwo3lem1 7429  qsqueeze 7461  icoshft 7577  indstr 7630  elfzlem 7643  fsequb 7702  cau3iri 8167  cau5i 8171  iserzex 8395  cvgratlem2ALT 8510  infpn2 8778  tgval3 8895  iincld 8955  sncld 9064  lmuni 9229  bcthlem14 9290  gapm 9462  lnon0 9798  pilem1 10020  indexfi 10174  dif1card 10177  fbunfip 10282  filrn 10293  hausfillim 10303  ocnel 10803  h1dn0 11108  osumlem5 11217  nmcopexlem1 11588  nmcfnexlem1 11617  cnlnssadj 11650  cvnbtwn2 11859  cvnbtwn3 11860  cvnbtwn4 11861  dmdbr2 11875  dmdbr3 11877  dmdbr4 11878  superpos 11926  atcvati 11958  mdsymlem4 11978  sumdmdii 11987  cdj3lem1 12006  bnj876 12803  bnj1284 13482  divalglem5 13700  ndvdssub 13710  coprm 13782  untangtr 13802  3orel2 13806  elres 13824  dfon2lem6 13854  dfon2lem7 13855  nofv 13998  axdenselem4 14022  axdenselem7 14025  axfelem12 14042  islatalg 14531  elsubops 14877  altretop 14997  iintlem1 15010  mtord 15346  dmsdtriordOLD 15360  trer 15361  elicc3 15362  onsdomOLD 15385  hscptsscld 15434  alexsublem4 15440  reconnlem1 15446  reconnlem4 15449  reconn 15451  locfincomp 15514  comppfsc 15517  neibastop2lem4 15522  fnemeet1 15528  ist1-3 15543  filufint 15574  flimfnfcls 15615  tailuni 15638  filnet 15645  indexfiOLD 15755  fdc 15812  incsequz 15815  txmet 15925  sstotbnd 15936  totbndss 15937  heiborlem37 15991  0ring 16175  dmncan1 16224  bicomdd 16228  prtlem90 16246  prtlem16 16272  prtlem15 16281  ax12 16367  cla4gft 16406  joinlem 16817  meetlem 16824  hlrelat2 17052  cvrat 17062  linepsub 17232

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 164

Copyright terms: Public domain