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  4518  elinsn  4714  tppreqb  4808  sotri2  6128  sotri3  6129  somincom  6133  fnun  6661  fvmpti  6995  ovigg  7550  ndmovg  7587  onint  7775  ordsucOLD  7799  tfindsg  7847  findsg  7887  zfrep6  7938  poxp2  8126  extmptsuppeq  8170  tfrlem9  8382  tfr3  8396  omlimcl  8575  oneo  8578  nnneo  8651  pssnn  9165  onomeneq  9225  pssnnOLD  9262  inficl  9417  frmin  9741  updjud  9926  dfac2b  10122  axdc2lem  10440  axextnd  10583  canthp1lem2  10645  gchinf  10649  inatsk  10770  indpi  10899  ltaddpr2  11027  reclem2pr  11040  supsrlem  11103  axrrecex  11155  zeo  12645  nn0ind-raph  12659  fzm1  13578  fzind2  13747  addmodlteq  13908  bcpasc  14278  pr2pwpr  14437  swrdnnn0nd  14603  pwdif  15811  oddnn02np1  16288  oddge22np1  16289  evennn02n  16290  evennn2n  16291  bitsfzo  16373  bezoutlem1  16478  algcvgblem  16511  coprmdvds1  16586  qredeq  16591  prmreclem2  16847  ramtcl2  16941  divsfval  17490  joinval  18327  meetval  18341  gsumval3  19770  pgpfac1lem3a  19941  fiinopn  22395  restntr  22678  lly1stc  22992  dgradd2  25774  dgrcolem2  25780  asinneg  26381  ftalem2  26568  ftalem4  26570  ftalem5  26571  bpos1lem  26775  zabsle1  26789  lgsqrmodndvds  26846  incistruhgr  28329  fusgrfis  28577  uhgrnbgr0nb  28601  cusgrrusgr  28828  wlkswwlksf1o  29123  isclwwlknx  29279  clwwlknwwlksnb  29298  clwlknf1oclwwlknlem1  29324  frgrwopreglem3  29557  frgrreg  29637  frgrregord013  29638  h1de2ctlem  30796  pjclem4a  31439  pj3lem1  31447  chrelat2i  31606  sumdmdii  31656  elim2if  31764  bnj1468  33846  bnj517  33885  acycgrislfgr  34132  axextdist  34760  funtransport  34992  bj-19.21t0  35697  bj-projval  35866  areacirc  36570  rngoueqz  36797  isdmn3  36931  ax12fromc15  37764  lkrlspeqN  38030  hlrelat2  38263  ps-1  38337  dalem54  38586  cdleme42c  39332  dihmeetlem6  40169  oe0suclim  42013  sdomne0  42150  sdomne0d  42151  frege124d  42498  uneqsn  42762  iotavalb  43175  natglobalincr  45578  2reuimp  45810  afv2orxorb  45923  iccpartnel  46093  fargshiftf1  46096  gbowge7  46418  sbgoldbwt  46432  bgoldbtbndlem1  46460  uspgrsprf1  46512