HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version
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
StepHypRef Expression
1 syl6bir.1 . . 3 |- (ph -> (ch <-> ps))
21biimprd 154 . 2 |- (ph -> (ps -> ch))
3 syl6bir.2 . 2 |- (ch -> th)
42, 3syl6 22 1 |- (ph -> (ps -> th))
Colors of variables: wff set class
Syntax hints:   -> wi 3   <-> wb 146
This theorem is referenced by:  19.33b 1088  ax11 1214  reuuni1 2872  onint 2996  ordsuc 3055  findsg 3147  tfindsg 3152  fneu 3578  fnun 3580  zfrep6 3600  tz6.12i 3726  tfrlem9 3904  tfr3 3911  ndmoprg 4028  ndmoprgOLD 4029  dfoprab5 4099  omlimcl 4193  oneo 4196  pssnn 4513  aceq6b 4714  carddom 4808  axextnd 4915  indpi 5006  ltexpq 5052  ltexpq2 5053  nsmallpq 5055  ltbtwnpq 5056  ltaddpr2 5113  ltexpri 5121  reclem2pr 5129  suppsr2 5195  axrnegex 5255  axrrecex 5256  zeot 6146  nn0ind-raph 6162  cru 6667  fsumcmpndx2 6980  cncnplem2 7714  cncnplem3 7715  bcthlem29 7961  h1de2ctlem 9394  lnopcon 9878  lnfncon 9905  pjclem4a 10036  pj3lem1 10044  chrelat2 10200  sumdmdi 10249  fiiu2 10377  filintf 10443  filint2 10446
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