Theorem syl6bir 255

Description: A mixed syllogism inference. (Contributed by NM, 18-May-1994.)

Hypotheses

Ref	Expression
syl6bir.1	⊢ (𝜑 → (𝜒 ↔ 𝜓))
syl6bir.2	⊢ (𝜒 → 𝜃)

Assertion

Ref	Expression
syl6bir	⊢ (𝜑 → (𝜓 → 𝜃))

Proof of Theorem syl6bir

Step	Hyp	Ref	Expression
1		syl6bir.1	. . 3 ⊢ (𝜑 → (𝜒 ↔ 𝜓))
2	1	biimprd 249	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
3		syl6bir.2	. 2 ⊢ (𝜒 → 𝜃)
4	2, 3	syl6 35	1 ⊢ (𝜑 → (𝜓 → 𝜃))

Syntax hints:   → wi 4   ↔ wb 207

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 208

This theorem is referenced by:  ralnralall  4378  elinsn  4559  tppreqb  4651  sotri2  5872  sotri3  5873  somincom  5877  fnun  6340  fvmpti  6641  ovigg  7158  ndmovg  7194  onint  7373  ordsuc  7392  tfindsg  7438  findsg  7472  zfrep6  7519  extmptsuppeq  7712  tfrlem9  7880  tfr3  7894  omlimcl  8061  oneo  8064  nnneo  8135  pssnn  8589  inficl  8742  updjud  9216  dfac2b  9409  axdc2lem  9723  axextnd  9866  canthp1lem2  9928  gchinf  9932  inatsk  10053  indpi  10182  ltaddpr2  10310  reclem2pr  10323  supsrlem  10386  axrrecex  10438  zeo  11922  nn0ind-raph  11936  fzm1  12841  fzind2  13009  addmodlteq  13168  bcpasc  13535  pr2pwpr  13687  swrdnnn0nd  13858  pwdif  15060  oddnn02np1  15534  oddge22np1  15535  evennn02n  15536  evennn2n  15537  bitsfzo  15621  bezoutlem1  15720  algcvgblem  15754  coprmdvds1  15829  qredeq  15834  prmreclem2  16086  ramtcl2  16180  divsfval  16653  joinval  17448  meetval  17462  gsumval3  18752  pgpfac1lem3a  18919  fiinopn  21197  restntr  21478  lly1stc  21792  dgradd2  24545  dgrcolem2  24551  asinneg  25149  ftalem2  25337  ftalem4  25339  ftalem5  25340  bpos1lem  25544  zabsle1  25558  lgsqrmodndvds  25615  incistruhgr  26551  fusgrfis  26799  uhgrnbgr0nb  26823  cusgrrusgr  27050  wlkswwlksf1o  27343  isclwwlknx  27500  clwwlknwwlksnb  27520  clwlknf1oclwwlknlem1  27546  frgrwopreglem3  27781  frgrreg  27861  frgrregord013  27862  h1de2ctlem  29019  pjclem4a  29662  pj3lem1  29670  chrelat2i  29829  sumdmdii  29879  elim2if  29984  bnj1468  31730  bnj517  31769  acycgrislfgr  32009  axextdist  32655  funtransport  33103  bj-19.21t0  33729  bj-projval  33934  areacirc  34539  rngoueqz  34771  isdmn3  34905  ax12fromc15  35593  lkrlspeqN  35859  hlrelat2  36091  ps-1  36165  dalem54  36414  cdleme42c  37160  dihmeetlem6  37997  frege124d  39612  uneqsn  39879  iotavalb  40321  2reuimp  42852  afv2orxorb  42965  iccpartnel  43102  fargshiftf1  43105  gbowge7  43432  sbgoldbwt  43446  bgoldbtbndlem1  43474  uspgrsprf1  43526