Theorem syl6ib 212

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

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

This theorem is referenced by:  pm3.37 286  exp4a 378  pm5.18 658  19.23 1059  19.29 1067  cbvexd 1316  ax15 1352  2eu3 1444  necon2bd 1607  necon4bd 1619  necon4d 1620  reupick 2269  sspr 2466  trin 2680  pwssun 2816  efrirr 2918  wefrc 2933  onfr 2976  onmindif2 3051  suc11 3083  ssrel 3237  elreldm 3327  iss 3381  xp11 3463  ssrnres 3467  opelf 3625  dffo4 3805  mapsn 4329  en2d 4381  nneneq 4492  unblem1 4517  supnub 4556  suc11reg 4577  inf3lem2 4586  trcl 4617  tz9.13 4635  aceq5lem5 4711  entri 4811  unxpdomlem 4815  carduniima 4862  cardinfima 4863  alephval2 4874  distrlem2pr 5100  ltapr 5123  suppsrlem 5193  suppsr2 5195  suprelem 5231  ssxr 5513  ngtmnftt 5540  sup2 5998  nnunb 6017  elnn0nn 6118  nneo 6144  uzwo3lem1 6164  qsqueeze 6218  icoshft 6341  indstr 6393  elfzlem 6405  fsequb 6455  cau3ir 6852  cau5 6856  iserzext 7071  cvgratlem2ALT 7183  infpn2 7452  tgval3t 7567  iincld 7621  sncld 7726  lmuni 7886  bcthlem14 7946  pilem1 8590  ocnelt 9086  h1dn0 9390  osumlem5 9499  nmcopexlem1 9866  nmcfnexlem1 9895  cnlnssadj 9928  cvnbtwn2t 10124  cvnbtwn3t 10125  cvnbtwn4t 10126  dmdbr2 10140  dmdbr3 10141  dmdbr4 10142  superpos 10189  atcvat 10221  mdsymlem4 10241  sumdmdi 10249  cdj3lem1 10266  iintlem1 10476

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 147

Copyright terms: Public domain