Theorem syl6bir 233

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

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

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 189

This theorem is referenced by:  19.21t  1988  axext3  2435  tppreqb  4116  issref  5216  sotri2  5232  sotri3  5233  somincom  5237  ordelinel  5524  fnun  5687  fvmpti  5952  ovigg  6422  ndmovg  6457  onint  6627  ordsuc  6646  tfindsg  6692  findsg  6725  zfrep6  6766  extmptsuppeq  6944  tfrlem9  7108  tfr3  7122  omlimcl  7284  oneo  7287  nnneo  7357  pssnn  7795  inficl  7944  dfac2  8566  axdc2lem  8883  axextnd  9021  canthp1lem2  9083  gchinf  9087  inatsk  9208  indpi  9337  ltaddpr2  9465  reclem2pr  9478  supsrlem  9540  axrrecex  9592  zeo  11028  nn0ind-raph  11042  fzm1  11881  fzind2  12030  bcpasc  12513  pr2pwpr  12643  bitsfzo  14421  bezoutlem1  14515  algcvgblem  14548  qredeq  14675  prmreclem2  14873  ramtcl2  14978  ramtcl2OLD  14979  divsfval  15465  joinval  16263  meetval  16277  gsumval3  17553  pgpfac1lem3a  17721  fiinopn  19943  restntr  20210  lly1stc  20523  dgradd2  23234  dgrcolem2  23240  asinneg  23824  ftalem2  24010  ftalem4  24012  ftalem5  24013  ftalem4OLD  24014  ftalem5OLD  24015  bpos1lem  24222  wlkdvspthlem  25349  fargshiftf1  25377  wlknwwlknsur  25452  wlkiswwlksur  25459  clwlkfoclwwlk  25585  hashnbgravdg  25653  cusgraisrusgra  25678  frgrareg  25857  frgraregord013  25858  rngoueqz  26170  h1de2ctlem  27220  pjclem4a  27863  pj3lem1  27871  chrelat2i  28030  sumdmdii  28080  elim2if  28173  bnj1468  29669  bnj517  29708  axextdist  30458  funtransport  30810  bj-19.21t  31444  bj-projval  31602  wl-ax12  31925  areacirc  32049  isdmn3  32319  ax12  32487  lkrlspeqN  32749  hlrelat2  32980  ps-1  33054  dalem54  33303  cdleme42c  34051  dihmeetlem6  34889  frege124d  36365  iotavalb  36792  iccpartnel  38762  gboge7  38874  bgoldbwt  38888  bgoldbtbndlem1  38910  ralnralall  38995  incistruhgr  39181  fusgrfis  39406  uhgrnbgr0nb  39432  cusgrrusgr  39607