Theorem sylbird 252

Description: A syllogism deduction. (Contributed by NM, 3-Aug-1994.)

Hypotheses

Ref	Expression
sylbird.1	⊢ (𝜑 → (𝜒 ↔ 𝜓))
sylbird.2	⊢ (𝜑 → (𝜒 → 𝜃))

Assertion

Ref	Expression
sylbird	⊢ (𝜑 → (𝜓 → 𝜃))

Proof of Theorem sylbird

Step	Hyp	Ref	Expression
1		sylbird.1	. . 3 ⊢ (𝜑 → (𝜒 ↔ 𝜓))
2	1	biimprd 240	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
3		sylbird.2	. 2 ⊢ (𝜑 → (𝜒 → 𝜃))
4	2, 3	syld 47	1 ⊢ (𝜑 → (𝜓 → 𝜃))

Syntax hints:   → wi 4   ↔ wb 198

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 199

This theorem is referenced by:  3imtr3d  285  ceqex  3554  eqreu  3628  sotr2  5350  sossfld  5877  ordintdif  6072  tz6.12i  6519  f1cofveqaeqALT  6836  soisoi  6898  riotaeqimp  6954  ov3  7121  tfindsg  7385  tfindsg2  7386  nnsuc  7407  findsg  7418  suppssr  7657  tfrlem9  7818  oe0lem  7932  oa00  7978  omwordi  7990  om00  7994  omass  7999  oelim2  8014  oeoa  8016  oeoe  8018  nnmwordi  8054  swoso  8114  dom2lem  8338  onsdominel  8454  f1finf1o  8532  cantnfp1lem3  8929  cantnfp1  8930  cantnflem1  8938  rankr1ai  9013  rankval3b  9041  harcard  9193  infxpenlem  9225  alephnbtwn  9283  alephinit  9307  infxp  9427  cofsmo  9481  infpssALT  9525  fin23lem24  9534  fin56  9605  ttukeylem6  9726  ficard  9777  alephval2  9784  fpwwe2lem8  9849  fpwwe2  9855  gchdju1  9868  pwfseqlem3  9872  pwfseqlem4a  9873  pwfseqlem4  9874  gchpwdom  9882  tskss  9970  inar1  9987  gruss  10008  gruurn  10010  ltsonq  10181  distrlem4pr  10238  sqgt0sr  10318  map2psrpr  10322  letric  10532  renegcli  10740  addid0  10852  mulge0b  11303  nnge1  11461  0mnnnnn0  11734  nn0lt2  11851  zneo  11871  uzind2  11881  fzind  11886  nn0ind-raph  11888  uzwo  12118  nn01to3  12148  zbtwnre  12153  rpnnen1lem5  12188  ledivge1le  12270  xrletri  12356  qsqueeze  12404  difreicc  12679  elfzmlbp  12827  difelfznle  12830  elfzodifsumelfzo  12911  ssfzo12  12938  elfzonelfzo  12947  flflp1  12985  fleqceilz  13030  modsumfzodifsn  13120  addmodlteq  13122  om2uzf1oi  13129  expnngt1  13410  facdiv  13455  facwordi  13457  bcpasc  13489  hashdom  13546  hashdmpropge2  13642  ccatsymb  13735  swrdnnn0nd  13814  swrdnd0  13815  swrdsbslen  13831  swrdspsleq  13832  swrdlsw  13835  pfxnd0  13860  swrdswrdlem  13876  swrdccatin1  13914  swrdccatin12lem3  13923  swrdccat  13928  pfxccat3a  13932  repswswrd  13993  cshwidx0  14020  cshwcsh2id  14042  limsupbnd1  14690  lo1bdd2  14732  addcn2  14801  mulcn2  14803  o1rlimmul  14826  lo1add  14834  lo1mul  14835  rlimno1  14861  ruclem3  15436  odd2np1  15540  oddge22np1  15548  bitsfzo  15634  cncongr1  15857  2mulprm  15883  prm23ge5  15998  pcdvdsb  16051  pcaddlem  16070  infpnlem1  16092  prmunb  16096  vdwlem9  16171  vdwnnlem3  16179  ramcl  16211  prmgaplem5  16237  cshwshash  16284  setcmon  17195  setcepi  17196  setciso  17199  ghmf1  18148  sylow2alem2  18494  sylow2blem3  18498  qusabl  18731  lt6abl  18759  cyggexb  18763  gsumcom2  18838  imasring  19082  f1ghm0to0  19205  f1rhm0to0OLD  19206  drnginvrcl  19232  drnginvrl  19234  drnginvrr  19235  subrgdvds  19262  lsmelval2  19569  quscrng  19724  mplsubrglem  19923  gsummoncoe1  20165  xrsdsreclblem  20283  obs2ss  20565  obslbs  20566  mp2pm2mplem4  21111  chfacfisf  21156  chfacfisfcpmat  21157  cayleyhamilton1  21194  cmpsublem  21701  cmpsub  21702  1stccnp  21764  locfincf  21833  txhaus  21949  xkohaus  21955  ufilss  22207  cfinufil  22230  fmfnfmlem1  22256  hausflim  22283  fclscf  22327  alexsubb  22348  qustgplem  22422  prdsbl  22794  metss2lem  22814  nghmcn  23047  cfil3i  23565  cmetcaulem  23584  minveclem4  23728  ovolgelb  23774  ovolunnul  23794  ovoliun  23799  ovoliunnul  23801  ovolicc2lem2  23812  iundisj2  23843  voliunlem3  23846  rolle  24280  dvlip  24283  lhop1lem  24303  lhop2  24305  dvfsumrlim  24321  deg1ge  24385  coeeulem  24507  dgrco  24558  radcnvlt1  24699  psercnlem1  24706  logcnlem2  24917  logcnlem3  24918  cxpeq  25029  angpined  25099  efrlim  25239  dmgmaddn0  25292  lgamucov  25307  basellem2  25351  ppieq0  25445  mumullem2  25449  chpeq0  25476  chteq0  25477  chtub  25480  fsumvma  25481  dchrptlem1  25532  bposlem6  25557  gausslemma2dlem0i  25632  gausslemma2dlem1a  25633  lgseisenlem2  25644  2sqlem6  25691  2sq2  25701  2sqnn0  25706  2sqreulem1  25714  2sqreunnlem1  25717  dchrisum0lem1  25784  pntrsumbnd2  25835  pntlem3  25877  colinearalg  26389  eengtrkg  26465  incistruhgr  26557  wlkv0  27125  crctcshwlkn0  27297  clwlkclwwlklem2a4  27493  clwlkclwwlklem2  27496  clwlkclwwlkfoOLD  27509  clwlkclwwlkfo  27513  eucrctshift  27763  frrusgrord0  27864  frgrreg  27941  blocni  28349  ubthlem1  28415  minvecolem4  28425  shmodsi  28937  atcvati  29934  atcvat2i  29935  chirredlem4  29941  atmd2  29948  sumdmdlem  29966  addltmulALT  29994  iundisj2f  30096  iundisj2fi  30258  rngurd  30492  erdszelem9  31991  sotr3  32462  rdgprc  32500  soseq  32557  noextenddif  32636  nosupno  32664  nosupbnd1  32675  noetalem3  32680  scutun12  32732  slerec  32738  cgrsub  32967  btwnxfr  32978  lineext  32998  linecgr  33003  btwnconn1lem4  33012  btwnconn1lem5  33013  btwnconn1lem6  33014  btwnconn1lem8  33016  btwnconn1lem11  33019  mptsnunlem  33996  finxpreclem6  34053  ltflcei  34269  poimirlem23  34304  poimirlem24  34305  poimirlem31  34312  poimirlem32  34313  ftc1anclem5  34360  heiborlem6  34484  grpokerinj  34561  dvrunz  34622  isdmn3  34742  dmncan1  34744  l1cvpat  35583  atnle  35846  cvlexch3  35861  cvlexch4N  35862  cvlatexchb1  35863  cvrat2  35958  atlelt  35967  3dimlem4a  35992  3dimlem4OLDN  35994  ps-1  36006  ps-2  36007  4atlem10  36135  4atlem11  36138  4atlem12  36141  cdleme11c  36790  cdleme21c  36856  cdlemg6d  37150  trlcoat  37252  tendoid0  37354  cdleml3N  37507  dia2dimlem7  37599  pellexlem1  38767  pellexlem6  38772  imasgim  39041  iunrelexpmin1  39361  iunrelexpmin2  39365  radcnvrat  40006  nzss  40009  elprneb  42615  or2expropbi  42620  tz6.12i-afv2  42794  dfatcolem  42806  f1oresf1o2  42842  zm1nn  42854  2ffzoeq  42880  sfprmdvdsmersenne  43076  lighneallem3  43080  lighneallem4  43083  requad01  43094  fppr2odd  43204  fpprwppr  43212  stgoldbwt  43249  sbgoldbaltlem1  43252  isomuspgrlem1  43300  lmod0rng  43443  0ring1eq0  43447  lidldomn1  43496  rngciso  43557  rngcisoALTV  43569  ringciso  43608  ringcisoALTV  43632  ztprmneprm  43699  lincresunit3  43843  itsclc0yqsol  44059  itschlc0xyqsol1  44061  aacllem  44209