Theorem sylbird 260

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 248	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
3		sylbird.2	. 2 ⊢ (𝜑 → (𝜒 → 𝜃))
4	2, 3	syld 47	1 ⊢ (𝜑 → (𝜓 → 𝜃))

Syntax hints:   → wi 4   ↔ wb 206

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 207

This theorem is referenced by:  3imtr3d  293  ceqex  3604  eqreu  3685  sotr2  5563  sotr3  5570  sossfld  6141  ordintdif  6365  tz6.12i  6857  f1cofveqaeqALT  7201  soisoi  7271  riotaeqimp  7338  ov3  7518  tfindsg  7800  tfindsg2  7801  nnsuc  7823  findsg  7836  soseq  8098  suppssr  8134  suppssrg  8135  tfrlem9  8313  oe0lem  8437  oa00  8483  omwordi  8495  om00  8499  omass  8504  oelim2  8519  oeoa  8521  oeoe  8523  nnmwordi  8559  swoso  8665  dom2lem  8924  onsdominel  9049  f1finf1o  9167  fiint  9221  cantnfp1lem3  9580  cantnfp1  9581  cantnflem1  9589  ttrclselem2  9626  rankr1ai  9701  rankval3b  9729  harcard  9881  infxpenlem  9914  alephnbtwn  9972  alephinit  9996  infxp  10115  cofsmo  10170  infpssALT  10214  fin23lem24  10223  fin56  10294  ttukeylem6  10415  ficard  10466  alephval2  10473  fpwwe2lem7  10538  fpwwe2  10544  gchdju1  10557  pwfseqlem3  10561  pwfseqlem4a  10562  pwfseqlem4  10563  gchpwdom  10571  tskss  10659  inar1  10676  gruss  10697  gruurn  10699  ltsonq  10870  distrlem4pr  10927  sqgt0sr  11007  map2psrpr  11011  letric  11223  renegcli  11432  addid0  11546  mulge0b  12002  nnge1  12163  0mnnnnn0  12423  nn0lt2  12546  zneo  12566  uzind2  12576  fzind  12581  nn0ind-raph  12583  uzwo  12819  nn01to3  12849  zbtwnre  12854  rpnnen1lem5  12889  ledivge1le  12973  xrletri  13062  qsqueeze  13110  difreicc  13394  elfzmlbp  13549  difelfznle  13552  elfzodifsumelfzo  13641  ssfzo12  13669  elfzonelfzo  13679  flflp1  13721  fleqceilz  13768  modsumfzodifsn  13861  addmodlteq  13863  om2uzf1oi  13870  expnngt1  14158  facdiv  14204  facwordi  14206  bcpasc  14238  hashdom  14296  hashgt23el  14341  hashdmpropge2  14400  ccatsymb  14500  swrdnnn0nd  14574  swrdnd0  14575  swrdsbslen  14582  swrdspsleq  14583  swrdlsw  14585  pfxnd0  14606  swrdswrdlem  14621  swrdccatin1  14642  pfxccatin12lem3  14649  swrdccat  14652  pfxccat3a  14655  repswswrd  14701  cshwidx0  14723  cshwcsh2id  14745  limsupbnd1  15399  lo1bdd2  15441  addcn2  15511  mulcn2  15513  o1rlimmul  15536  lo1add  15544  lo1mul  15545  rlimno1  15571  ruclem3  16152  odd2np1  16262  oddge22np1  16270  bitsfzo  16356  cncongr1  16588  2mulprm  16614  prm23ge5  16737  pcdvdsb  16791  pcaddlem  16810  infpnlem1  16832  prmunb  16836  vdwlem9  16911  vdwnnlem3  16919  ramcl  16951  prmgaplem5  16977  cshwshash  17026  setcmon  18004  setcepi  18005  setciso  18008  xpsmnd0  18696  f1ghm0to0  19167  ghmf1  19168  sylow2alem2  19540  sylow2blem3  19544  qusabl  19787  lt6abl  19817  cyggexb  19821  gsumcom2  19897  ringurd  20113  imasring  20258  xpsring1d  20261  0ring1eq0  20458  subrgdvds  20511  rngciso  20563  ringciso  20597  isdomn4  20641  drnginvrcl  20678  drnginvrl  20681  drnginvrr  20682  lsmelval2  21029  quscrng  21230  xrsdsreclblem  21359  obs2ss  21676  obslbs  21677  rnasclassa  21842  mplsubrglem  21951  psdmul  22091  gsummoncoe1  22233  mp2pm2mplem4  22734  chfacfisf  22779  chfacfisfcpmat  22780  cayleyhamilton1  22817  cmpsublem  23324  cmpsub  23325  1stccnp  23387  locfincf  23456  txhaus  23572  xkohaus  23578  ufilss  23830  cfinufil  23853  fmfnfmlem1  23879  hausflim  23906  fclscf  23950  alexsubb  23971  qustgplem  24046  prdsbl  24416  metss2lem  24436  nghmcn  24670  cfil3i  25206  cmetcaulem  25225  minveclem4  25369  ovolgelb  25418  ovolunnul  25438  ovoliun  25443  ovoliunnul  25445  ovolicc2lem2  25456  iundisj2  25487  voliunlem3  25490  rolle  25931  dvlip  25935  lhop1lem  25955  lhop2  25957  dvfsumrlim  25975  deg1ge  26040  coeeulem  26166  dgrco  26218  radcnvlt1  26364  psercnlem1  26372  logcnlem2  26589  logcnlem3  26590  cxpeq  26704  angpined  26777  efrlim  26916  efrlimOLD  26917  dmgmaddn0  26970  lgamucov  26985  basellem2  27029  ppieq0  27123  mumullem2  27127  chpeq0  27156  chteq0  27157  chtub  27160  fsumvma  27161  dchrptlem1  27212  bposlem6  27237  gausslemma2dlem0i  27312  gausslemma2dlem1a  27313  lgseisenlem2  27324  2sqlem6  27371  2sq2  27381  2sqnn0  27386  2sqreulem1  27394  2sqreunnlem1  27397  dchrisum0lem1  27464  pntrsumbnd2  27515  pntlem3  27557  noextenddif  27617  nosupno  27652  nosupbnd1  27663  noinfno  27667  noinfbnd1  27678  noetasuplem4  27685  noetainflem4  27689  scutun12  27761  slerec  27770  cutlt  27886  sleadd2im  27941  onsiso  28215  n0sfincut  28292  colinearalg  28899  eengtrkg  28975  incistruhgr  29068  wlkv0  29639  crctcshwlkn0  29810  clwwlkccatlem  29980  clwlkclwwlklem2a4  29988  clwlkclwwlklem2  29991  clwlkclwwlkfo  30000  eucrctshift  30234  frrusgrord0  30331  frgrreg  30385  blocni  30796  ubthlem1  30861  minvecolem4  30871  shmodsi  31380  atcvati  32377  atcvat2i  32378  chirredlem4  32384  atmd2  32391  sumdmdlem  32409  addltmulALT  32437  iundisj2f  32581  iundisj2fi  32790  f1resveqaeq  35108  erdszelem9  35254  satffunlem1lem2  35458  satffunlem2lem2  35461  rdgprc  35847  cgrsub  36100  btwnxfr  36111  lineext  36131  linecgr  36136  btwnconn1lem4  36145  btwnconn1lem5  36146  btwnconn1lem6  36147  btwnconn1lem8  36149  btwnconn1lem11  36152  mptsnunlem  37393  finxpreclem6  37451  ltflcei  37658  poimirlem23  37693  poimirlem24  37694  poimirlem31  37701  poimirlem32  37702  ftc1anclem5  37747  heiborlem6  37866  grpokerinj  37943  dvrunz  38004  isdmn3  38124  dmncan1  38126  membpartlem19  38919  l1cvpat  39163  atnle  39426  cvlexch3  39441  cvlexch4N  39442  cvlatexchb1  39443  cvrat2  39538  atlelt  39547  3dimlem4a  39572  3dimlem4OLDN  39574  ps-1  39586  ps-2  39587  4atlem10  39715  4atlem11  39718  4atlem12  39721  cdleme11c  40370  cdleme21c  40436  cdlemg6d  40730  trlcoat  40832  tendoid0  40934  cdleml3N  41087  dia2dimlem7  41179  aks6d1c6lem3  42275  expeq1d  42432  fsuppind  42698  pellexlem1  42936  pellexlem6  42941  imasgim  43207  onsupmaxb  43346  safesnsupfidom1o  43524  reabsifnpos  43740  reabsifnneg  43742  iunrelexpmin1  43815  iunrelexpmin2  43819  radcnvrat  44421  nzss  44424  pwclaxpow  45091  ormkglobd  46987  elprneb  47143  or2expropbi  47148  tz6.12i-afv2  47357  dfatcolem  47369  f1oresf1o2  47405  zm1nn  47416  2ffzoeq  47441  modmkpkne  47475  sfprmdvdsmersenne  47717  lighneallem3  47721  lighneallem4  47724  requad01  47735  fppr2odd  47845  fpprwppr  47853  stgoldbwt  47890  sbgoldbaltlem1  47893  isuspgrimlem  48009  upgrimpthslem2  48022  isubgr3stgrlem4  48083  isubgr3stgrlem7  48086  gpg5nbgrvtx03starlem1  48182  gpg5nbgrvtx03starlem3  48184  gpg5nbgrvtx13starlem1  48185  gpg5nbgrvtx13starlem3  48187  lmod0rng  48343  lidldomn1  48345  rngcisoALTV  48391  ringcisoALTV  48425  ztprmneprm  48461  lincresunit3  48596  itsclc0yqsol  48879  itschlc0xyqsol1  48881  aacllem  49916