Theorem syl6bir 254

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  4519  elinsn  4715  tppreqb  4809  sotri2  6131  sotri3  6132  somincom  6136  fnun  6664  fvmpti  6998  ovigg  7553  ndmovg  7590  onint  7778  ordsucOLD  7802  tfindsg  7850  findsg  7890  zfrep6  7941  poxp2  8129  extmptsuppeq  8173  tfrlem9  8385  tfr3  8399  omlimcl  8578  oneo  8581  nnneo  8654  pssnn  9168  onomeneq  9228  pssnnOLD  9265  inficl  9420  frmin  9744  updjud  9929  dfac2b  10125  axdc2lem  10443  axextnd  10586  canthp1lem2  10648  gchinf  10652  inatsk  10773  indpi  10902  ltaddpr2  11030  reclem2pr  11043  supsrlem  11106  axrrecex  11158  zeo  12648  nn0ind-raph  12662  fzm1  13581  fzind2  13750  addmodlteq  13911  bcpasc  14281  pr2pwpr  14440  swrdnnn0nd  14606  pwdif  15814  oddnn02np1  16291  oddge22np1  16292  evennn02n  16293  evennn2n  16294  bitsfzo  16376  bezoutlem1  16481  algcvgblem  16514  coprmdvds1  16589  qredeq  16594  prmreclem2  16850  ramtcl2  16944  divsfval  17493  joinval  18330  meetval  18344  gsumval3  19775  pgpfac1lem3a  19946  fiinopn  22403  restntr  22686  lly1stc  23000  dgradd2  25782  dgrcolem2  25788  asinneg  26391  ftalem2  26578  ftalem4  26580  ftalem5  26581  bpos1lem  26785  zabsle1  26799  lgsqrmodndvds  26856  incistruhgr  28339  fusgrfis  28587  uhgrnbgr0nb  28611  cusgrrusgr  28838  wlkswwlksf1o  29133  isclwwlknx  29289  clwwlknwwlksnb  29308  clwlknf1oclwwlknlem1  29334  frgrwopreglem3  29567  frgrreg  29647  frgrregord013  29648  h1de2ctlem  30808  pjclem4a  31451  pj3lem1  31459  chrelat2i  31618  sumdmdii  31668  elim2if  31776  bnj1468  33857  bnj517  33896  acycgrislfgr  34143  axextdist  34771  funtransport  35003  bj-19.21t0  35708  bj-projval  35877  areacirc  36581  rngoueqz  36808  isdmn3  36942  ax12fromc15  37775  lkrlspeqN  38041  hlrelat2  38274  ps-1  38348  dalem54  38597  cdleme42c  39343  dihmeetlem6  40180  oe0suclim  42027  sdomne0  42164  sdomne0d  42165  frege124d  42512  uneqsn  42776  iotavalb  43189  natglobalincr  45591  2reuimp  45823  afv2orxorb  45936  iccpartnel  46106  fargshiftf1  46109  gbowge7  46431  sbgoldbwt  46445  bgoldbtbndlem1  46473  uspgrsprf1  46525