Theorem syl6bir 215

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

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

This theorem is referenced by:  19.33b 1090  ax11 1217  reuuni1 2877  onint 3001  ordsuc 3060  findsg 3152  tfindsg 3157  fneu 3584  fnun 3586  zfrep6 3606  tz6.12i 3732  tfrlem9 3910  tfr3 3917  ndmoprg 4034  ndmoprgOLD 4035  dfoprab5 4105  omlimcl 4199  oneo 4202  pssnn 4519  aceq6b 4722  carddom 4816  axextnd 4923  indpi 5014  ltexpq 5060  ltexpq2 5061  nsmallpq 5063  ltbtwnpq 5064  ltaddpr2 5121  ltexpri 5129  reclem2pr 5137  suppsr2 5203  axrnegex 5263  axrrecex 5264  zeot 6154  nn0ind-raph 6170  cru 6675  fsumcmpndx2 6988  cncnplem2 7725  cncnplem3 7726  bcthlem29 7977  h1de2ctlem 9417  lnopcon 9901  lnfncon 9928  pjclem4a 10064  pj3lem1 10072  chrelat2 10229  sumdmdi 10278  fiiu2 10413  filintf 10479  filint2 10482

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