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  1909  ax12  2236  axext3  2434  tppreqb  4157  reusv6OLD  4648  ordelinel  4965  issref  5368  sotri2  5384  sotri3  5385  somincom  5389  fnun  5669  fvmpti  5930  ovigg  6396  ndmovg  6431  onint  6603  ordsuc  6622  tfindsg  6668  findsg  6700  zfrep6  6741  extmptsuppeq  6916  tfrlem9  7046  tfr3  7060  omlimcl  7219  oneo  7222  nnneo  7292  pssnn  7731  inficl  7877  dfac2  8502  axdc2lem  8819  axextnd  8957  canthp1lem2  9020  gchinf  9024  inatsk  9145  indpi  9274  ltaddpr2  9402  reclem2pr  9415  supsrlem  9477  axrrecex  9529  zeo  10944  nn0ind-raph  10960  fzm1  11762  fzind2  11905  bcpasc  12384  pr2pwpr  12507  bitsfzo  14172  bezoutlem1  14263  algcvgblem  14293  qredeq  14334  prmreclem2  14522  ramtcl2  14616  divsfval  15039  joinval  15837  meetval  15851  gsumval3OLD  17110  gsumval3  17113  pgpfac1lem3a  17325  fiinopn  19580  restntr  19853  lly1stc  20166  dgradd2  22834  dgrcolem2  22840  asinneg  23417  ftalem2  23548  ftalem4  23550  ftalem5  23551  bpos1lem  23758  wlkdvspthlem  24814  fargshiftf1  24842  wlknwwlknsur  24917  wlkiswwlksur  24924  clwlkfoclwwlk  25050  hashnbgravdg  25118  cusgraisrusgra  25143  frgrareg  25322  frgraregord013  25323  rngoueqz  25633  h1de2ctlem  26674  pjclem4a  27318  pj3lem1  27326  chrelat2i  27485  sumdmdii  27535  elim2if  27631  axextdist  29475  funtransport  29912  areacirc  30355  isdmn3  30714  iotavalb  31581  ralnralall  32687  bnj1468  34324  bnj517  34363  bj-19.21t  34823  bj-projval  34974  lkrlspeqN  35312  hlrelat2  35543  ps-1  35617  dalem54  35866  cdleme42c  36614  dihmeetlem6  37452