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  3595  eqreu  3676  sotr2  5573  sotr3  5580  sossfld  6151  ordintdif  6375  tz6.12i  6867  f1cofveqaeqALT  7213  soisoi  7283  riotaeqimp  7350  ov3  7530  tfindsg  7812  tfindsg2  7813  nnsuc  7835  findsg  7848  soseq  8109  suppssr  8145  suppssrg  8146  tfrlem9  8324  oe0lem  8448  oa00  8494  omwordi  8506  om00  8510  omass  8515  oelim2  8531  oeoa  8533  oeoe  8535  nnmwordi  8571  swoso  8678  dom2lem  8939  onsdominel  9064  f1finf1o  9183  fiint  9237  cantnfp1lem3  9601  cantnfp1  9602  cantnflem1  9610  ttrclselem2  9647  rankr1ai  9722  rankval3b  9750  harcard  9902  infxpenlem  9935  alephnbtwn  9993  alephinit  10017  infxp  10136  cofsmo  10191  infpssALT  10235  fin23lem24  10244  fin56  10315  ttukeylem6  10436  ficard  10487  alephval2  10495  fpwwe2lem7  10560  fpwwe2  10566  gchdju1  10579  pwfseqlem3  10583  pwfseqlem4a  10584  pwfseqlem4  10585  gchpwdom  10593  tskss  10681  inar1  10698  gruss  10719  gruurn  10721  ltsonq  10892  distrlem4pr  10949  sqgt0sr  11029  map2psrpr  11033  letric  11246  renegcli  11455  addid0  11569  mulge0b  12026  nnge1  12205  0mnnnnn0  12469  nn0lt2  12592  zneo  12612  uzind2  12622  fzind  12627  nn0ind-raph  12629  uzwo  12861  nn01to3  12891  zbtwnre  12896  rpnnen1lem5  12931  ledivge1le  13015  xrletri  13104  qsqueeze  13153  difreicc  13437  elfzmlbp  13593  difelfznle  13596  elfzodifsumelfzo  13686  ssfzo12  13714  elfzonelfzo  13724  flflp1  13766  fleqceilz  13813  modsumfzodifsn  13906  addmodlteq  13908  om2uzf1oi  13915  expnngt1  14203  facdiv  14249  facwordi  14251  bcpasc  14283  hashdom  14341  hashgt23el  14386  hashdmpropge2  14445  ccatsymb  14545  swrdnnn0nd  14619  swrdnd0  14620  swrdsbslen  14627  swrdspsleq  14628  swrdlsw  14630  pfxnd0  14651  swrdswrdlem  14666  swrdccatin1  14687  pfxccatin12lem3  14694  swrdccat  14697  pfxccat3a  14700  repswswrd  14746  cshwidx0  14768  cshwcsh2id  14790  limsupbnd1  15444  lo1bdd2  15486  addcn2  15556  mulcn2  15558  o1rlimmul  15581  lo1add  15589  lo1mul  15590  rlimno1  15616  ruclem3  16200  odd2np1  16310  oddge22np1  16318  bitsfzo  16404  cncongr1  16636  2mulprm  16662  prm23ge5  16786  pcdvdsb  16840  pcaddlem  16859  infpnlem1  16881  prmunb  16885  vdwlem9  16960  vdwnnlem3  16968  ramcl  17000  prmgaplem5  17026  cshwshash  17075  setcmon  18054  setcepi  18055  setciso  18058  xpsmnd0  18746  f1ghm0to0  19220  ghmf1  19221  sylow2alem2  19593  sylow2blem3  19597  qusabl  19840  lt6abl  19870  cyggexb  19874  gsumcom2  19950  ringurd  20166  imasring  20310  xpsring1d  20313  0ring1eq0  20510  subrgdvds  20563  rngciso  20615  ringciso  20649  isdomn4  20693  drnginvrcl  20730  drnginvrl  20733  drnginvrr  20734  lsmelval2  21080  quscrng  21281  xrsdsreclblem  21393  obs2ss  21709  obslbs  21710  rnasclassa  21875  mplsubrglem  21982  psdmul  22132  gsummoncoe1  22273  mp2pm2mplem4  22774  chfacfisf  22819  chfacfisfcpmat  22820  cayleyhamilton1  22857  cmpsublem  23364  cmpsub  23365  1stccnp  23427  locfincf  23496  txhaus  23612  xkohaus  23618  ufilss  23870  cfinufil  23893  fmfnfmlem1  23919  hausflim  23946  fclscf  23990  alexsubb  24011  qustgplem  24086  prdsbl  24456  metss2lem  24476  nghmcn  24710  cfil3i  25236  cmetcaulem  25255  minveclem4  25399  ovolgelb  25447  ovolunnul  25467  ovoliun  25472  ovoliunnul  25474  ovolicc2lem2  25485  iundisj2  25516  voliunlem3  25519  rolle  25957  dvlip  25960  lhop1lem  25980  lhop2  25982  dvfsumrlim  25998  deg1ge  26063  coeeulem  26189  dgrco  26240  radcnvlt1  26383  psercnlem1  26390  logcnlem2  26607  logcnlem3  26608  cxpeq  26721  angpined  26794  efrlim  26933  dmgmaddn0  26986  lgamucov  27001  basellem2  27045  ppieq0  27139  mumullem2  27143  chpeq0  27171  chteq0  27172  chtub  27175  fsumvma  27176  dchrptlem1  27227  bposlem6  27252  gausslemma2dlem0i  27327  gausslemma2dlem1a  27328  lgseisenlem2  27339  2sqlem6  27386  2sq2  27396  2sqnn0  27401  2sqreulem1  27409  2sqreunnlem1  27412  dchrisum0lem1  27479  pntrsumbnd2  27530  pntlem3  27572  noextenddif  27632  nosupno  27667  nosupbnd1  27678  noinfno  27682  noinfbnd1  27693  noetasuplem4  27700  noetainflem4  27704  cutsun12  27782  lesrec  27791  cutlt  27924  leadds2im  27980  oniso  28263  n0fincut  28347  bdayfinbndlem1  28459  z12bdaylem1  28462  colinearalg  28979  eengtrkg  29055  incistruhgr  29148  wlkv0  29718  crctcshwlkn0  29889  clwwlkccatlem  30059  clwlkclwwlklem2a4  30067  clwlkclwwlklem2  30070  clwlkclwwlkfo  30079  eucrctshift  30313  frrusgrord0  30410  frgrreg  30464  blocni  30876  ubthlem1  30941  minvecolem4  30951  shmodsi  31460  atcvati  32457  atcvat2i  32458  chirredlem4  32464  atmd2  32471  sumdmdlem  32489  addltmulALT  32517  iundisj2f  32660  iundisj2fi  32870  f1resveqaeq  35228  erdszelem9  35381  satffunlem1lem2  35585  satffunlem2lem2  35588  rdgprc  35974  cgrsub  36227  btwnxfr  36238  lineext  36258  linecgr  36263  btwnconn1lem4  36272  btwnconn1lem5  36273  btwnconn1lem6  36274  btwnconn1lem8  36276  btwnconn1lem11  36279  mh-inf3f1  36723  mptsnunlem  37654  finxpreclem6  37712  ltflcei  37929  poimirlem23  37964  poimirlem24  37965  poimirlem31  37972  poimirlem32  37973  ftc1anclem5  38018  heiborlem6  38137  grpokerinj  38214  dvrunz  38275  isdmn3  38395  dmncan1  38397  membpartlem19  39235  l1cvpat  39500  atnle  39763  cvlexch3  39778  cvlexch4N  39779  cvlatexchb1  39780  cvrat2  39875  atlelt  39884  3dimlem4a  39909  3dimlem4OLDN  39911  ps-1  39923  ps-2  39924  4atlem10  40052  4atlem11  40055  4atlem12  40058  cdleme11c  40707  cdleme21c  40773  cdlemg6d  41067  trlcoat  41169  tendoid0  41271  cdleml3N  41424  dia2dimlem7  41516  aks6d1c6lem3  42611  expeq1d  42756  fsuppind  43023  pellexlem1  43257  pellexlem6  43262  imasgim  43528  onsupmaxb  43667  safesnsupfidom1o  43844  reabsifnpos  44060  reabsifnneg  44062  iunrelexpmin1  44135  iunrelexpmin2  44139  radcnvrat  44741  nzss  44744  pwclaxpow  45411  ormkglobd  47303  elprneb  47471  or2expropbi  47476  tz6.12i-afv2  47685  dfatcolem  47697  f1oresf1o2  47733  zm1nn  47744  2ffzoeq  47770  modmkpkne  47809  sfprmdvdsmersenne  48060  lighneallem3  48064  lighneallem4  48067  requad01  48091  fppr2odd  48201  fpprwppr  48209  stgoldbwt  48246  sbgoldbaltlem1  48249  isuspgrimlem  48365  upgrimpthslem2  48378  isubgr3stgrlem4  48439  isubgr3stgrlem7  48442  gpg5nbgrvtx03starlem1  48538  gpg5nbgrvtx03starlem3  48540  gpg5nbgrvtx13starlem1  48541  gpg5nbgrvtx13starlem3  48543  lmod0rng  48699  lidldomn1  48701  rngcisoALTV  48747  ringcisoALTV  48781  ztprmneprm  48817  lincresunit3  48951  itsclc0yqsol  49234  itschlc0xyqsol1  49236  aacllem  50270