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 1092  ax11 1219  reuuni1 2882  onint 3006  ordsuc 3065  findsg 3157  tfindsg 3162  fneu 3592  fnun 3594  zfrep6 3614  tz6.12i 3741  tfrlem9 3919  tfr3 3926  ndmoprg 4043  dfoprab5 4115  omlimcl 4209  oneo 4212  pssnn 4534  aceq6b 4742  carddom 4836  axextnd 4943  indpi 5034  ltexpq 5080  ltexpq2 5081  nsmallpq 5083  ltbtwnpq 5084  ltaddpr2 5141  ltexpri 5149  reclem2pr 5157  suppsr2 5223  axrnegex 5283  axrrecex 5284  zeot 6199  nn0ind-raph 6214  cru 6737  fsumcmpndx2 7042  cncnplem2 7775  cncnplem3 7776  bcthlem29 8027  h1de2ctlem 9478  lnopcon 9963  lnfncon 9990  pjclem4a 10126  pj3lem1 10134  chrelat2 10292  sumdmdi 10342  fiiu2 10488  fiiu2OLD 10489  filintf 10569  filint2 10574  filint2OLD 10575

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