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  4446  elinsn  4643  tppreqb  4735  sotri2  6023  sotri3  6024  somincom  6028  fnun  6529  fvmpti  6856  ovigg  7396  ndmovg  7433  onint  7617  ordsuc  7636  tfindsg  7682  findsg  7720  zfrep6  7771  extmptsuppeq  7975  tfrlem9  8187  tfr3  8201  omlimcl  8371  oneo  8374  nnneo  8445  pssnn  8913  pssnnOLD  8969  inficl  9114  updjud  9623  dfac2b  9817  axdc2lem  10135  axextnd  10278  canthp1lem2  10340  gchinf  10344  inatsk  10465  indpi  10594  ltaddpr2  10722  reclem2pr  10735  supsrlem  10798  axrrecex  10850  zeo  12336  nn0ind-raph  12350  fzm1  13265  fzind2  13433  addmodlteq  13594  bcpasc  13963  pr2pwpr  14121  swrdnnn0nd  14297  pwdif  15508  oddnn02np1  15985  oddge22np1  15986  evennn02n  15987  evennn2n  15988  bitsfzo  16070  bezoutlem1  16175  algcvgblem  16210  coprmdvds1  16285  qredeq  16290  prmreclem2  16546  ramtcl2  16640  divsfval  17175  joinval  18010  meetval  18024  gsumval3  19423  pgpfac1lem3a  19594  fiinopn  21958  restntr  22241  lly1stc  22555  dgradd2  25334  dgrcolem2  25340  asinneg  25941  ftalem2  26128  ftalem4  26130  ftalem5  26131  bpos1lem  26335  zabsle1  26349  lgsqrmodndvds  26406  incistruhgr  27352  fusgrfis  27600  uhgrnbgr0nb  27624  cusgrrusgr  27851  wlkswwlksf1o  28145  isclwwlknx  28301  clwwlknwwlksnb  28320  clwlknf1oclwwlknlem1  28346  frgrwopreglem3  28579  frgrreg  28659  frgrregord013  28660  h1de2ctlem  29818  pjclem4a  30461  pj3lem1  30469  chrelat2i  30628  sumdmdii  30678  elim2if  30788  bnj1468  32726  bnj517  32765  acycgrislfgr  33014  axextdist  33681  poxp2  33717  poxp3  33723  funtransport  34260  bj-19.21t0  34940  bj-projval  35113  areacirc  35797  rngoueqz  36025  isdmn3  36159  ax12fromc15  36846  lkrlspeqN  37112  hlrelat2  37344  ps-1  37418  dalem54  37667  cdleme42c  38413  dihmeetlem6  39250  frege124d  41258  uneqsn  41522  iotavalb  41937  2reuimp  44494  afv2orxorb  44607  iccpartnel  44778  fargshiftf1  44781  gbowge7  45103  sbgoldbwt  45117  bgoldbtbndlem1  45145  uspgrsprf1  45197