Theorem syl6bir 244

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

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

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 197

This theorem is referenced by:  19.21tOLDOLD  2074  19.21tOLD  2213  ax12OLD  2341  axext3  2604  ralnralall  4080  elinsn  4245  tppreqb  4336  issref  5509  sotri2  5525  sotri3  5526  somincom  5530  ordelinelOLD  5826  fnun  5997  fvmpti  6281  ovigg  6781  ndmovg  6817  onint  6995  ordsuc  7014  tfindsg  7060  findsg  7093  zfrep6  7134  extmptsuppeq  7319  tfrlem9  7481  tfr3  7495  omlimcl  7658  oneo  7661  nnneo  7731  pssnn  8178  inficl  8331  dfac2  8953  axdc2lem  9270  axextnd  9413  canthp1lem2  9475  gchinf  9479  inatsk  9600  indpi  9729  ltaddpr2  9857  reclem2pr  9870  supsrlem  9932  axrrecex  9984  zeo  11463  nn0ind-raph  11477  fzm1  12420  fzind2  12586  addmodlteq  12745  bcpasc  13108  pr2pwpr  13261  oddnn02np1  15072  oddge22np1  15073  evennn02n  15074  evennn2n  15075  bitsfzo  15157  bezoutlem1  15256  algcvgblem  15290  coprmdvds1  15365  qredeq  15371  prmreclem2  15621  ramtcl2  15715  divsfval  16207  joinval  17005  meetval  17019  gsumval3  18308  pgpfac1lem3a  18475  fiinopn  20706  restntr  20986  lly1stc  21299  dgradd2  24024  dgrcolem2  24030  asinneg  24613  ftalem2  24800  ftalem4  24802  ftalem5  24803  bpos1lem  25007  zabsle1  25021  lgsqrmodndvds  25078  incistruhgr  25974  fusgrfis  26222  uhgrnbgr0nb  26250  cusgrrusgr  26477  wlkpwwlkf1ouspgr  26765  wlknwwlksnsur  26776  wlkwwlksur  26783  clwlksfoclwwlk  26963  frgrwopreglem3  27178  frgrreg  27252  frgrregord013  27253  h1de2ctlem  28414  pjclem4a  29057  pj3lem1  29065  chrelat2i  29224  sumdmdii  29274  elim2if  29363  bnj1468  30916  bnj517  30955  axextdist  31705  funtransport  32138  bj-19.21t  32817  bj-projval  32984  areacirc  33505  rngoueqz  33739  isdmn3  33873  ax12fromc15  34190  lkrlspeqN  34458  hlrelat2  34689  ps-1  34763  dalem54  35012  cdleme42c  35760  dihmeetlem6  36598  frege124d  38053  uneqsn  38321  iotavalb  38631  iccpartnel  41374  fargshiftf1  41377  pwdif  41501  gbowge7  41651  sbgoldbwt  41665  bgoldbtbndlem1  41693  uspgrsprf1  41755