Theorem syl6bir 232

Description: A mixed syllogism inference. (Contributed by NM, 18-May-1994.)

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

Syntax hints:   -> wi 4   <-> wb 187

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 188

This theorem is referenced by:  19.21t  1959  axext3  2402  tppreqb  4138  issref  5228  sotri2  5244  sotri3  5245  somincom  5249  ordelinel  5536  fnun  5696  fvmpti  5959  ovigg  6427  ndmovg  6462  onint  6632  ordsuc  6651  tfindsg  6697  findsg  6730  zfrep6  6771  extmptsuppeq  6946  tfrlem9  7107  tfr3  7121  omlimcl  7283  oneo  7286  nnneo  7356  pssnn  7792  inficl  7941  dfac2  8561  axdc2lem  8878  axextnd  9016  canthp1lem2  9078  gchinf  9082  inatsk  9203  indpi  9332  ltaddpr2  9460  reclem2pr  9473  supsrlem  9535  axrrecex  9587  zeo  11021  nn0ind-raph  11035  fzm1  11874  fzind2  12022  bcpasc  12505  pr2pwpr  12632  bitsfzo  14396  bezoutlem1  14490  algcvgblem  14523  qredeq  14650  prmreclem2  14848  ramtcl2  14953  ramtcl2OLD  14954  divsfval  15440  joinval  16238  meetval  16252  gsumval3  17528  pgpfac1lem3a  17696  fiinopn  19917  restntr  20184  lly1stc  20497  dgradd2  23208  dgrcolem2  23214  asinneg  23798  ftalem2  23984  ftalem4  23986  ftalem5  23987  ftalem4OLD  23988  ftalem5OLD  23989  bpos1lem  24196  wlkdvspthlem  25322  fargshiftf1  25350  wlknwwlknsur  25425  wlkiswwlksur  25432  clwlkfoclwwlk  25558  hashnbgravdg  25626  cusgraisrusgra  25651  frgrareg  25830  frgraregord013  25831  rngoueqz  26143  h1de2ctlem  27193  pjclem4a  27836  pj3lem1  27844  chrelat2i  28003  sumdmdii  28053  elim2if  28150  bnj1468  29652  bnj517  29691  axextdist  30440  funtransport  30790  bj-19.21t  31389  bj-projval  31545  wl-ax12  31826  areacirc  31950  isdmn3  32220  ax12  32393  lkrlspeqN  32655  hlrelat2  32886  ps-1  32960  dalem54  33209  cdleme42c  33957  dihmeetlem6  34795  frege124d  36212  iotavalb  36638  iccpartnel  38463  gboge7  38575  bgoldbwt  38589  bgoldbtbndlem1  38611  ralnralall  38692