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  1836  ax12  2206  tppreqb  4002  reusv6OLD  4491  ordelinel  4804  issref  5199  sotri2  5215  sotri3  5216  somincom  5223  fnun  5505  fvmpti  5761  ovigg  6200  ndmovg  6235  onint  6395  ordsuc  6414  tfindsg  6460  findsg  6492  zfrep6  6534  extmptsuppeq  6702  tfrlem9  6830  tfr3  6844  omlimcl  7005  oneo  7008  nnneo  7078  pssnn  7519  inficl  7663  dfac2  8288  axdc2lem  8605  axextnd  8743  canthp1lem2  8807  gchinf  8811  inatsk  8932  indpi  9063  ltaddpr2  9191  reclem2pr  9204  supsrlem  9265  axrrecex  9317  zeo  10714  nn0ind-raph  10729  fzind2  11620  bcpasc  12080  pr2pwpr  12166  bitsfzo  13613  bezoutlem1  13704  algcvgblem  13734  qredeq  13774  prmreclem2  13960  ramtcl2  14054  divsfval  14467  joinval  15157  meetval  15171  gsumval3OLD  16361  gsumval3  16364  pgpfac1lem3a  16550  fiinopn  18355  restntr  18627  lly1stc  18941  dgradd2  21619  dgrcolem2  21625  asinneg  22165  ftalem2  22295  ftalem4  22297  ftalem5  22298  bpos1lem  22505  wlkdvspthlem  23328  fargshiftf1  23345  hashnbgravdg  23403  rngoueqz  23739  h1de2ctlem  24780  pjclem4a  25424  pj3lem1  25432  chrelat2i  25591  sumdmdii  25641  elim2if  25729  axextdist  27459  funtransport  27908  areacirc  28330  isdmn3  28715  iotavalb  29526  ralnralall  29961  wlknwwlknsur  30187  wlkiswwlksur  30194  clwlkfoclwwlk  30361  cusgraisrusgra  30394  frgrareg  30553  frgraregord013  30554  bnj1468  31538  bnj517  31577  bj-19.21t  31955  bj-projval  32069  lkrlspeqN  32386  hlrelat2  32617  ps-1  32691  dalem54  32940  cdleme42c  33686  dihmeetlem6  34524