Theorem syl6bir 256

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

Syntax hints:   → wi 4   ↔ wb 208

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 209

This theorem is referenced by:  ralnralall  4456  elinsn  4638  tppreqb  4730  sotri2  5982  sotri3  5983  somincom  5987  fnun  6456  fvmpti  6760  ovigg  7287  ndmovg  7323  onint  7502  ordsuc  7521  tfindsg  7567  findsg  7601  zfrep6  7648  extmptsuppeq  7846  tfrlem9  8013  tfr3  8027  omlimcl  8196  oneo  8199  nnneo  8270  pssnn  8728  inficl  8881  updjud  9355  dfac2b  9548  axdc2lem  9862  axextnd  10005  canthp1lem2  10067  gchinf  10071  inatsk  10192  indpi  10321  ltaddpr2  10449  reclem2pr  10462  supsrlem  10525  axrrecex  10577  zeo  12060  nn0ind-raph  12074  fzm1  12979  fzind2  13147  addmodlteq  13306  bcpasc  13673  pr2pwpr  13829  swrdnnn0nd  14010  pwdif  15215  oddnn02np1  15689  oddge22np1  15690  evennn02n  15691  evennn2n  15692  bitsfzo  15776  bezoutlem1  15879  algcvgblem  15913  coprmdvds1  15988  qredeq  15993  prmreclem2  16245  ramtcl2  16339  divsfval  16812  joinval  17607  meetval  17621  gsumval3  19019  pgpfac1lem3a  19190  fiinopn  21501  restntr  21782  lly1stc  22096  dgradd2  24850  dgrcolem2  24856  asinneg  25456  ftalem2  25643  ftalem4  25645  ftalem5  25646  bpos1lem  25850  zabsle1  25864  lgsqrmodndvds  25921  incistruhgr  26856  fusgrfis  27104  uhgrnbgr0nb  27128  cusgrrusgr  27355  wlkswwlksf1o  27649  isclwwlknx  27806  clwwlknwwlksnb  27826  clwlknf1oclwwlknlem1  27852  frgrwopreglem3  28085  frgrreg  28165  frgrregord013  28166  h1de2ctlem  29324  pjclem4a  29967  pj3lem1  29975  chrelat2i  30134  sumdmdii  30184  elim2if  30291  bnj1468  32111  bnj517  32150  acycgrislfgr  32392  axextdist  33037  funtransport  33485  bj-19.21t0  34146  bj-projval  34301  areacirc  34979  rngoueqz  35210  isdmn3  35344  ax12fromc15  36033  lkrlspeqN  36299  hlrelat2  36531  ps-1  36605  dalem54  36854  cdleme42c  37600  dihmeetlem6  38437  frege124d  40097  uneqsn  40364  iotavalb  40753  2reuimp  43305  afv2orxorb  43418  iccpartnel  43589  fargshiftf1  43592  gbowge7  43919  sbgoldbwt  43933  bgoldbtbndlem1  43961  uspgrsprf1  44013