Theorem syl6bir 253

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 247	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
3		syl6bir.2	. 2 ⊢ (𝜒 → 𝜃)
4	2, 3	syl6 35	1 ⊢ (𝜑 → (𝜓 → 𝜃))

Syntax hints:   → wi 4   ↔ wb 205

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 206

This theorem is referenced by:  ralnralall  4518  elinsn  4714  tppreqb  4808  sotri2  6130  sotri3  6131  somincom  6135  fnun  6663  fvmpti  6997  ovigg  7555  ndmovg  7592  onint  7780  ordsucOLD  7804  tfindsg  7852  findsg  7892  zfrep6  7943  poxp2  8131  extmptsuppeq  8175  tfrlem9  8387  tfr3  8401  omlimcl  8580  oneo  8583  nnneo  8656  pssnn  9170  onomeneq  9230  pssnnOLD  9267  inficl  9422  frmin  9746  updjud  9931  dfac2b  10127  axdc2lem  10445  axextnd  10588  canthp1lem2  10650  gchinf  10654  inatsk  10775  indpi  10904  ltaddpr2  11032  reclem2pr  11045  supsrlem  11108  axrrecex  11160  zeo  12652  nn0ind-raph  12666  fzm1  13585  fzind2  13754  addmodlteq  13915  bcpasc  14285  pr2pwpr  14444  swrdnnn0nd  14610  pwdif  15818  oddnn02np1  16295  oddge22np1  16296  evennn02n  16297  evennn2n  16298  bitsfzo  16380  bezoutlem1  16485  algcvgblem  16518  coprmdvds1  16593  qredeq  16598  prmreclem2  16854  ramtcl2  16948  divsfval  17497  joinval  18334  meetval  18348  gsumval3  19816  pgpfac1lem3a  19987  fiinopn  22623  restntr  22906  lly1stc  23220  dgradd2  26006  dgrcolem2  26012  asinneg  26615  ftalem2  26802  ftalem4  26804  ftalem5  26805  bpos1lem  27009  zabsle1  27023  lgsqrmodndvds  27080  incistruhgr  28594  fusgrfis  28842  uhgrnbgr0nb  28866  cusgrrusgr  29093  wlkswwlksf1o  29388  isclwwlknx  29544  clwwlknwwlksnb  29563  clwlknf1oclwwlknlem1  29589  frgrwopreglem3  29822  frgrreg  29902  frgrregord013  29903  h1de2ctlem  31063  pjclem4a  31706  pj3lem1  31714  chrelat2i  31873  sumdmdii  31923  elim2if  32031  bnj1468  34143  bnj517  34182  acycgrislfgr  34429  axextdist  35063  funtransport  35295  bj-19.21t0  36011  bj-projval  36180  areacirc  36884  rngoueqz  37111  isdmn3  37245  ax12fromc15  38078  lkrlspeqN  38344  hlrelat2  38577  ps-1  38651  dalem54  38900  cdleme42c  39646  dihmeetlem6  40483  oe0suclim  42329  sdomne0  42466  sdomne0d  42467  frege124d  42814  uneqsn  43078  iotavalb  43491  natglobalincr  45890  2reuimp  46122  afv2orxorb  46235  iccpartnel  46405  fargshiftf1  46408  gbowge7  46730  sbgoldbwt  46744  bgoldbtbndlem1  46772  uspgrsprf1  46824