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  1888  ax12  2218  axext3  2421  tppreqb  4152  reusv6OLD  4644  ordelinel  4962  issref  5366  sotri2  5382  sotri3  5383  somincom  5390  fnun  5673  fvmpti  5936  ovigg  6404  ndmovg  6439  onint  6611  ordsuc  6630  tfindsg  6676  findsg  6708  zfrep6  6749  extmptsuppeq  6922  tfrlem9  7052  tfr3  7066  omlimcl  7225  oneo  7228  nnneo  7298  pssnn  7736  inficl  7883  dfac2  8509  axdc2lem  8826  axextnd  8964  canthp1lem2  9029  gchinf  9033  inatsk  9154  indpi  9283  ltaddpr2  9411  reclem2pr  9424  supsrlem  9486  axrrecex  9538  zeo  10949  nn0ind-raph  10964  fzind2  11898  bcpasc  12373  pr2pwpr  12494  bitsfzo  13957  bezoutlem1  14048  algcvgblem  14078  qredeq  14119  prmreclem2  14307  ramtcl2  14401  divsfval  14816  joinval  15504  meetval  15518  gsumval3OLD  16777  gsumval3  16780  pgpfac1lem3a  16995  fiinopn  19277  restntr  19549  lly1stc  19863  dgradd2  22530  dgrcolem2  22536  asinneg  23082  ftalem2  23212  ftalem4  23214  ftalem5  23215  bpos1lem  23422  wlkdvspthlem  24474  fargshiftf1  24502  wlknwwlknsur  24577  wlkiswwlksur  24584  clwlkfoclwwlk  24710  hashnbgravdg  24778  cusgraisrusgra  24803  frgrareg  24982  frgraregord013  24983  rngoueqz  25297  h1de2ctlem  26338  pjclem4a  26982  pj3lem1  26990  chrelat2i  27149  sumdmdii  27199  elim2if  27287  axextdist  29200  funtransport  29649  areacirc  30080  isdmn3  30439  iotavalb  31284  ralnralall  32128  bnj1468  33611  bnj517  33650  bj-19.21t  34115  bj-projval  34266  lkrlspeqN  34598  hlrelat2  34829  ps-1  34903  dalem54  35152  cdleme42c  35900  dihmeetlem6  36738