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  1852  ax12  2227  axext3  2447  tppreqb  4168  reusv6OLD  4658  ordelinel  4976  issref  5378  sotri2  5394  sotri3  5395  somincom  5402  fnun  5685  fvmpti  5947  ovigg  6405  ndmovg  6440  onint  6608  ordsuc  6627  tfindsg  6673  findsg  6705  zfrep6  6749  extmptsuppeq  6921  tfrlem9  7051  tfr3  7065  omlimcl  7224  oneo  7227  nnneo  7297  pssnn  7735  inficl  7881  dfac2  8507  axdc2lem  8824  axextnd  8962  canthp1lem2  9027  gchinf  9031  inatsk  9152  indpi  9281  ltaddpr2  9409  reclem2pr  9422  supsrlem  9484  axrrecex  9536  zeo  10942  nn0ind-raph  10957  fzind2  11888  bcpasc  12363  pr2pwpr  12482  bitsfzo  13940  bezoutlem1  14031  algcvgblem  14061  qredeq  14102  prmreclem2  14290  ramtcl2  14384  divsfval  14798  joinval  15488  meetval  15502  gsumval3OLD  16699  gsumval3  16702  pgpfac1lem3a  16917  fiinopn  19177  restntr  19449  lly1stc  19763  dgradd2  22399  dgrcolem2  22405  asinneg  22945  ftalem2  23075  ftalem4  23077  ftalem5  23078  bpos1lem  23285  wlkdvspthlem  24285  fargshiftf1  24313  wlknwwlknsur  24388  wlkiswwlksur  24395  clwlkfoclwwlk  24521  hashnbgravdg  24589  cusgraisrusgra  24614  frgrareg  24794  frgraregord013  24795  rngoueqz  25108  h1de2ctlem  26149  pjclem4a  26793  pj3lem1  26801  chrelat2i  26960  sumdmdii  27010  elim2if  27096  axextdist  28809  funtransport  29258  areacirc  29689  isdmn3  30074  iotavalb  30915  ralnralall  31761  bnj1468  32983  bnj517  33022  bj-19.21t  33484  bj-projval  33635  lkrlspeqN  33968  hlrelat2  34199  ps-1  34273  dalem54  34522  cdleme42c  35268  dihmeetlem6  36106