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  4517  elinsn  4713  tppreqb  4807  sotri2  6127  sotri3  6128  somincom  6132  fnun  6660  fvmpti  6994  ovigg  7549  ndmovg  7586  onint  7774  ordsucOLD  7798  tfindsg  7846  findsg  7886  zfrep6  7937  poxp2  8125  extmptsuppeq  8169  tfrlem9  8381  tfr3  8395  omlimcl  8574  oneo  8577  nnneo  8650  pssnn  9164  onomeneq  9224  pssnnOLD  9261  inficl  9416  frmin  9740  updjud  9925  dfac2b  10121  axdc2lem  10439  axextnd  10582  canthp1lem2  10644  gchinf  10648  inatsk  10769  indpi  10898  ltaddpr2  11026  reclem2pr  11039  supsrlem  11102  axrrecex  11154  zeo  12644  nn0ind-raph  12658  fzm1  13577  fzind2  13746  addmodlteq  13907  bcpasc  14277  pr2pwpr  14436  swrdnnn0nd  14602  pwdif  15810  oddnn02np1  16287  oddge22np1  16288  evennn02n  16289  evennn2n  16290  bitsfzo  16372  bezoutlem1  16477  algcvgblem  16510  coprmdvds1  16585  qredeq  16590  prmreclem2  16846  ramtcl2  16940  divsfval  17489  joinval  18326  meetval  18340  gsumval3  19769  pgpfac1lem3a  19940  fiinopn  22394  restntr  22677  lly1stc  22991  dgradd2  25773  dgrcolem2  25779  asinneg  26380  ftalem2  26567  ftalem4  26569  ftalem5  26570  bpos1lem  26774  zabsle1  26788  lgsqrmodndvds  26845  incistruhgr  28328  fusgrfis  28576  uhgrnbgr0nb  28600  cusgrrusgr  28827  wlkswwlksf1o  29122  isclwwlknx  29278  clwwlknwwlksnb  29297  clwlknf1oclwwlknlem1  29323  frgrwopreglem3  29556  frgrreg  29636  frgrregord013  29637  h1de2ctlem  30795  pjclem4a  31438  pj3lem1  31446  chrelat2i  31605  sumdmdii  31655  elim2if  31763  bnj1468  33845  bnj517  33884  acycgrislfgr  34131  axextdist  34759  funtransport  34991  bj-19.21t0  35696  bj-projval  35865  areacirc  36569  rngoueqz  36796  isdmn3  36930  ax12fromc15  37763  lkrlspeqN  38029  hlrelat2  38262  ps-1  38336  dalem54  38585  cdleme42c  39331  dihmeetlem6  40168  oe0suclim  42012  sdomne0  42149  sdomne0d  42150  frege124d  42497  uneqsn  42761  iotavalb  43174  natglobalincr  45577  2reuimp  45809  afv2orxorb  45922  iccpartnel  46092  fargshiftf1  46095  gbowge7  46417  sbgoldbwt  46431  bgoldbtbndlem1  46459  uspgrsprf1  46511