Theorem syl6bir 243

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

Syntax hints:   → wi 4   ↔ wb 195

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 196

This theorem is referenced by:  19.21t  2061  19.21tOLD  2201  ax12OLD  2329  axext3  2592  tppreqb  4277  issref  5428  sotri2  5444  sotri3  5445  somincom  5449  ordelinelOLD  5743  fnun  5911  fvmpti  6190  ovigg  6679  ndmovg  6715  onint  6887  ordsuc  6906  tfindsg  6952  findsg  6985  zfrep6  7027  extmptsuppeq  7206  tfrlem9  7368  tfr3  7382  omlimcl  7545  oneo  7548  nnneo  7618  pssnn  8063  inficl  8214  dfac2  8836  axdc2lem  9153  axextnd  9292  canthp1lem2  9354  gchinf  9358  inatsk  9479  indpi  9608  ltaddpr2  9736  reclem2pr  9749  supsrlem  9811  axrrecex  9863  zeo  11339  nn0ind-raph  11353  fzm1  12289  fzind2  12448  addmodlteq  12607  bcpasc  12970  pr2pwpr  13116  oddnn02np1  14910  oddge22np1  14911  evennn02n  14912  evennn2n  14913  bitsfzo  14995  bezoutlem1  15094  algcvgblem  15128  coprmdvds1  15203  qredeq  15209  prmreclem2  15459  ramtcl2  15553  divsfval  16030  joinval  16828  meetval  16842  gsumval3  18131  pgpfac1lem3a  18298  fiinopn  20531  restntr  20796  lly1stc  21109  dgradd2  23828  dgrcolem2  23834  asinneg  24413  ftalem2  24600  ftalem4  24602  ftalem5  24603  bpos1lem  24807  zabsle1  24821  lgsqrmodndvds  24878  incistruhgr  25746  wlkdvspthlem  26137  fargshiftf1  26165  wlknwwlknsur  26240  wlkiswwlksur  26247  clwlkfoclwwlk  26372  hashnbgravdg  26440  cusgraisrusgra  26465  frgrareg  26644  frgraregord013  26645  h1de2ctlem  27798  pjclem4a  28441  pj3lem1  28449  chrelat2i  28608  sumdmdii  28658  elim2if  28747  bnj1468  30170  bnj517  30209  axextdist  30949  funtransport  31308  bj-19.21t  32005  bj-projval  32177  areacirc  32675  rngoueqz  32909  isdmn3  33043  ax12fromc15  33208  lkrlspeqN  33476  hlrelat2  33707  ps-1  33781  dalem54  34030  cdleme42c  34778  dihmeetlem6  35616  frege124d  37072  uneqsn  37341  iotavalb  37653  iccpartnel  39976  pwdif  40039  gboge7  40185  bgoldbwt  40199  bgoldbtbndlem1  40221  ralnralall  40307  fusgrfis  40549  uhgrnbgr0nb  40576  cusgrrusgr  40781  1wlkpwwlkf1ouspgr  41076  wlknwwlksnsur  41087  wlkwwlksur  41094  clwlksfoclwwlk  41270  av-frgrareg  41548  av-frgraregord013  41549