Theorem sylbird 250

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

Syntax hints:   → wi 4   ↔ wb 196

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 197

This theorem is referenced by:  3imtr3d  282  ceqex  3333  eqreu  3398  sotr2  5064  sossfld  5580  ordtr3OLD  5770  ordintdif  5774  tz6.12i  6214  f1cofveqaeqALT  6516  soisoi  6578  riotaeqimp  6634  ov3  6797  tfindsg  7060  tfindsg2  7061  nnsuc  7082  findsg  7093  suppssr  7326  tfrlem9  7481  oe0lem  7593  oa00  7639  omwordi  7651  om00  7655  omass  7660  oelim2  7675  oeoa  7677  oeoe  7679  nnmwordi  7715  swoso  7775  dom2lem  7995  onsdominel  8109  f1finf1o  8187  cantnfp1lem3  8577  cantnfp1  8578  cantnflem1  8586  rankr1ai  8661  rankval3b  8689  harcard  8804  infxpenlem  8836  alephnbtwn  8894  alephinit  8918  infxp  9037  cofsmo  9091  infpssALT  9135  fin23lem24  9144  fin56  9215  ttukeylem6  9336  ficard  9387  alephval2  9394  fpwwe2lem8  9459  fpwwe2  9465  gchcda1  9478  pwfseqlem3  9482  pwfseqlem4a  9483  pwfseqlem4  9484  gchpwdom  9492  tskss  9580  inar1  9597  gruss  9618  gruurn  9620  ltsonq  9791  distrlem4pr  9848  sqgt0sr  9927  map2psrpr  9931  letric  10137  renegcli  10342  addid0  10450  mulge0b  10893  nnge1  11046  0mnnnnn0  11325  nn0lt2  11440  zneo  11460  uzind2  11470  fzind  11475  nn0ind-raph  11477  uzwo  11751  nn01to3  11781  zbtwnre  11786  rpnnen1lem5  11818  rpnnen1lem5OLD  11824  ledivge1le  11901  xrletri  11984  qsqueeze  12032  difreicc  12304  elfzmlbp  12450  difelfznle  12453  elfzodifsumelfzo  12533  ssfzo12  12561  elfzonelfzo  12570  flflp1  12608  fleqceilz  12653  modsumfzodifsn  12743  addmodlteq  12745  om2uzf1oi  12752  facdiv  13074  facwordi  13076  bcpasc  13108  hashdom  13168  hashdmpropge2  13265  ccatsymb  13366  swrdsbslen  13448  swrdspsleq  13449  swrdlsw  13452  swrdswrdlem  13459  swrdccatin1  13483  swrdccatin12lem3  13490  repswswrd  13531  cshwidx0  13552  cshwcsh2id  13574  limsupbnd1  14213  lo1bdd2  14255  addcn2  14324  mulcn2  14326  o1rlimmul  14349  lo1add  14357  lo1mul  14358  rlimno1  14384  znnenlem  14940  ruclem3  14962  odd2np1  15065  oddge22np1  15073  bitsfzo  15157  cncongr1  15381  prm23ge5  15520  pcdvdsb  15573  pcaddlem  15592  infpnlem1  15614  prmunb  15618  vdwlem9  15693  vdwnnlem3  15701  ramcl  15733  prmgaplem5  15759  cshwshash  15811  setcmon  16737  setcepi  16738  setciso  16741  ghmf1  17689  sylow2alem2  18033  sylow2blem3  18037  qusabl  18268  lt6abl  18296  cyggexb  18300  gsumcom2  18374  imasring  18619  f1rhm0to0  18740  drnginvrcl  18764  drnginvrl  18766  drnginvrr  18767  subrgdvds  18794  lsmelval2  19085  quscrng  19240  mplsubrglem  19439  gsummoncoe1  19674  xrsdsreclblem  19792  obs2ss  20073  obslbs  20074  mp2pm2mplem4  20614  chfacfisf  20659  chfacfisfcpmat  20660  cayleyhamilton1  20697  cmpsublem  21202  cmpsub  21203  1stccnp  21265  locfincf  21334  txhaus  21450  xkohaus  21456  ufilss  21709  cfinufil  21732  fmfnfmlem1  21758  hausflim  21785  fclscf  21829  alexsubb  21850  qustgplem  21924  prdsbl  22296  metss2lem  22316  nghmcn  22549  cfil3i  23067  cmetcaulem  23086  minveclem4  23203  ovolgelb  23248  ovolunnul  23268  ovoliun  23273  ovoliunnul  23275  ovolicc2lem2  23286  iundisj2  23317  voliunlem3  23320  rolle  23753  dvlip  23756  lhop1lem  23776  lhop2  23778  dvfsumrlim  23794  deg1ge  23858  coeeulem  23980  dgrco  24031  radcnvlt1  24172  psercnlem1  24179  logcnlem2  24389  logcnlem3  24390  cxpeq  24498  angpined  24557  efrlim  24696  dmgmaddn0  24749  lgamucov  24764  basellem2  24808  ppieq0  24902  mumullem2  24906  chpeq0  24933  chteq0  24934  chtub  24937  fsumvma  24938  dchrptlem1  24989  bposlem6  25014  gausslemma2dlem0i  25089  gausslemma2dlem1a  25090  lgseisenlem2  25101  2sqlem6  25148  dchrisum0lem1  25205  pntrsumbnd2  25256  pntlem3  25298  colinearalg  25790  eengtrkg  25865  incistruhgr  25974  wlkv0  26547  crctcshwlkn0  26713  clwlkclwwlklem2a4  26898  clwlkclwwlklem2  26901  eucrctshift  27103  frrusgrord0  27204  frgrreg  27252  blocni  27660  ubthlem1  27726  minvecolem4  27736  shmodsi  28248  atcvati  29245  atcvat2i  29246  chirredlem4  29252  atmd2  29259  sumdmdlem  29277  addltmulALT  29305  iundisj2f  29403  iundisj2fi  29556  rngurd  29788  erdszelem9  31181  sotr3  31656  rdgprc  31700  soseq  31751  noextenddif  31821  nosupno  31849  nosupbnd1  31860  noetalem3  31865  scutun12  31917  slerec  31923  cgrsub  32152  btwnxfr  32163  lineext  32183  linecgr  32188  btwnconn1lem4  32197  btwnconn1lem5  32198  btwnconn1lem6  32199  btwnconn1lem8  32201  btwnconn1lem11  32204  mptsnunlem  33185  finxpreclem6  33233  ltflcei  33397  poimirlem23  33432  poimirlem24  33433  poimirlem31  33440  poimirlem32  33441  ftc1anclem5  33489  heiborlem6  33615  grpokerinj  33692  dvrunz  33753  isdmn3  33873  dmncan1  33875  l1cvpat  34341  atnle  34604  cvlexch3  34619  cvlexch4N  34620  cvlatexchb1  34621  cvrat2  34715  atlelt  34724  3dimlem4a  34749  3dimlem4OLDN  34751  ps-1  34763  ps-2  34764  4atlem10  34892  4atlem11  34895  4atlem12  34898  cdleme11c  35548  cdleme21c  35615  cdlemg6d  35909  trlcoat  36011  tendoid0  36113  cdleml3N  36266  dia2dimlem7  36359  pellexlem1  37393  pellexlem6  37398  imasgim  37670  iunrelexpmin1  38000  iunrelexpmin2  38004  radcnvrat  38513  nzss  38516  elprneb  41296  zm1nn  41316  2ffzoeq  41338  pfxccat3a  41429  sfprmdvdsmersenne  41520  lighneallem3  41524  lighneallem4  41527  stgoldbwt  41664  sbgoldbaltlem1  41667  lmod0rng  41868  0ring1eq0  41872  lidldomn1  41921  rngciso  41982  rngcisoALTV  41994  ringciso  42033  ringcisoALTV  42057  ztprmneprm  42125  lincresunit3  42270  aacllem  42547