Theorem syl6bir 232

Description: A mixed syllogism inference.

Hypotheses

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

Assertion

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

Proof of Theorem syl6bir

Step	Hyp	Ref	Expression
1		syl6bir.1	. . 3 |- (ph -> (ch <-> ps))
2	1	biimprd 171	. 2 |- (ph -> (ps -> ch))
3		syl6bir.2	. 2 |- (ch -> th)
4	2, 3	syl6 25	1 |- (ph -> (ps -> th))

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

This theorem is referenced by:  19.33b 1444  19.33bOLD 1445  ax11 1589  reuuni1OLD 3809  eufromeq6 3833  onint 3876  ordsuc 3895  tfindsg 3944  findsg 3980  fneuOLD 4518  fnun 4520  zfrep6 4545  tz6.12i 4698  ndmoprg 4976  tfrlem9 5127  tfr3 5134  omlimcl 5257  oneo 5260  pssnn 5628  aceq6b 5904  carddom 5987  axextnd 6095  indpi 6186  ltexpq 6232  ltexpq2 6233  nsmallpq 6235  ltbtwnpq 6236  ltaddpr2 6293  ltexpri 6301  reclem2pr 6309  suppsr2 6375  axrnegex 6436  axrrecex 6437  zeo 7411  nn0ind-raph 7426  zindd 7427  crui 7987  fsumcmpndx2 8302  cncnplem2 9052  cncnplem3 9053  bcthlem29 9305  indexfi 10174  fiiu2 10220  filintf 10274  cncomp 10331  uznzr 10416  h1de2ctlem 11111  lnopconi 11600  lnfnconi 11627  pjclem4a 11771  pj3lem1 11779  chrelat2i 11937  sumdmdii 11987  bnj1009 12875  bnj1468 13145  bnj218 13250  axextdist 13866  repcpwti 14503  supdef 14604  gaplc 14731  filint2 14923  iscnp3 14946  mamb 15030  tarax3a 15222  tarax3f 15229  tartarmap 15265  subntr 15425  2ndcctbss 15478  fimax 15746  indexfiOLD 15755  totbndbnd 15944  isdmn3 16222  iotavalb 16394  hlrelat2 17052  ps-1 17078

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