Theorem syl6bir 229

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

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

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 185

This theorem is referenced by:  19.21t  1838  ax12  2205  tppreqb  4019  reusv6OLD  4508  ordelinel  4822  issref  5216  sotri2  5232  sotri3  5233  somincom  5240  fnun  5522  fvmpti  5778  ovigg  6216  ndmovg  6251  onint  6411  ordsuc  6430  tfindsg  6476  findsg  6508  zfrep6  6550  extmptsuppeq  6718  tfrlem9  6849  tfr3  6863  omlimcl  7022  oneo  7025  nnneo  7095  pssnn  7536  inficl  7680  dfac2  8305  axdc2lem  8622  axextnd  8760  canthp1lem2  8825  gchinf  8829  inatsk  8950  indpi  9081  ltaddpr2  9209  reclem2pr  9222  supsrlem  9283  axrrecex  9335  zeo  10732  nn0ind-raph  10747  fzind2  11642  bcpasc  12102  pr2pwpr  12188  bitsfzo  13636  bezoutlem1  13727  algcvgblem  13757  qredeq  13797  prmreclem2  13983  ramtcl2  14077  divsfval  14490  joinval  15180  meetval  15194  gsumval3OLD  16387  gsumval3  16390  pgpfac1lem3a  16582  fiinopn  18519  restntr  18791  lly1stc  19105  dgradd2  21740  dgrcolem2  21746  asinneg  22286  ftalem2  22416  ftalem4  22418  ftalem5  22419  bpos1lem  22626  wlkdvspthlem  23511  fargshiftf1  23528  hashnbgravdg  23586  rngoueqz  23922  h1de2ctlem  24963  pjclem4a  25607  pj3lem1  25615  chrelat2i  25774  sumdmdii  25824  elim2if  25911  axextdist  27618  funtransport  28067  areacirc  28494  isdmn3  28879  iotavalb  29689  ralnralall  30123  wlknwwlknsur  30349  wlkiswwlksur  30356  clwlkfoclwwlk  30523  cusgraisrusgra  30556  frgrareg  30715  frgraregord013  30716  bnj1468  31844  bnj517  31883  bj-19.21t  32343  bj-projval  32494  lkrlspeqN  32821  hlrelat2  33052  ps-1  33126  dalem54  33375  cdleme42c  34121  dihmeetlem6  34959