Theorem syl6bir 257

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

Syntax hints:   → wi 4   ↔ wb 209

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 210

This theorem is referenced by:  ralnralall  4416  elinsn  4612  tppreqb  4704  sotri2  5974  sotri3  5975  somincom  5979  fnun  6468  fvmpti  6795  ovigg  7332  ndmovg  7369  onint  7552  ordsuc  7571  tfindsg  7617  findsg  7655  zfrep6  7706  extmptsuppeq  7908  tfrlem9  8099  tfr3  8113  omlimcl  8284  oneo  8287  nnneo  8358  pssnn  8824  pssnnOLD  8872  inficl  9019  updjud  9515  dfac2b  9709  axdc2lem  10027  axextnd  10170  canthp1lem2  10232  gchinf  10236  inatsk  10357  indpi  10486  ltaddpr2  10614  reclem2pr  10627  supsrlem  10690  axrrecex  10742  zeo  12228  nn0ind-raph  12242  fzm1  13157  fzind2  13325  addmodlteq  13484  bcpasc  13852  pr2pwpr  14010  swrdnnn0nd  14186  pwdif  15395  oddnn02np1  15872  oddge22np1  15873  evennn02n  15874  evennn2n  15875  bitsfzo  15957  bezoutlem1  16062  algcvgblem  16097  coprmdvds1  16172  qredeq  16177  prmreclem2  16433  ramtcl2  16527  divsfval  17006  joinval  17837  meetval  17851  gsumval3  19246  pgpfac1lem3a  19417  fiinopn  21752  restntr  22033  lly1stc  22347  dgradd2  25116  dgrcolem2  25122  asinneg  25723  ftalem2  25910  ftalem4  25912  ftalem5  25913  bpos1lem  26117  zabsle1  26131  lgsqrmodndvds  26188  incistruhgr  27124  fusgrfis  27372  uhgrnbgr0nb  27396  cusgrrusgr  27623  wlkswwlksf1o  27917  isclwwlknx  28073  clwwlknwwlksnb  28092  clwlknf1oclwwlknlem1  28118  frgrwopreglem3  28351  frgrreg  28431  frgrregord013  28432  h1de2ctlem  29590  pjclem4a  30233  pj3lem1  30241  chrelat2i  30400  sumdmdii  30450  elim2if  30560  bnj1468  32493  bnj517  32532  acycgrislfgr  32781  axextdist  33445  poxp2  33470  poxp3  33476  funtransport  34019  bj-19.21t0  34699  bj-projval  34872  areacirc  35556  rngoueqz  35784  isdmn3  35918  ax12fromc15  36605  lkrlspeqN  36871  hlrelat2  37103  ps-1  37177  dalem54  37426  cdleme42c  38172  dihmeetlem6  39009  frege124d  40987  uneqsn  41251  iotavalb  41662  2reuimp  44222  afv2orxorb  44335  iccpartnel  44506  fargshiftf1  44509  gbowge7  44831  sbgoldbwt  44845  bgoldbtbndlem1  44873  uspgrsprf1  44925