Theorem sylbird 262

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 250	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
3		sylbird.2	. 2 ⊢ (𝜑 → (𝜒 → 𝜃))
4	2, 3	syld 47	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:  3imtr3d  295  ceqex  3606  eqreu  3686  sotr2  5582  sotr3  5589  sossfld  6161  ordintdif  6386  tz6.12i  6882  f1cofveqaeqALT  7231  soisoi  7301  riotaeqimp  7368  ov3  7548  tfindsg  7830  tfindsg2  7831  nnsuc  7853  findsg  7867  soseq  8127  suppssr  8163  suppssrg  8164  tfrlem9  8344  oe0lem  8470  oa00  8516  omwordi  8528  om00  8532  omass  8537  oelim2  8553  oeoa  8555  oeoe  8557  nnmwordi  8593  swoso  8701  dom2lem  8962  onsdominel  9087  f1finf1o  9206  fiint  9260  cantnfp1lem3  9625  cantnfp1  9626  cantnflem1  9634  ttrclselem2  9671  rankr1ai  9746  rankval3b  9774  harcard  9926  infxpenlem  9959  alephnbtwn  10017  alephinit  10041  infxp  10160  cofsmo  10216  infpssALT  10260  fin23lem24  10269  fin56  10340  ttukeylem6  10461  ficard  10512  alephval2  10520  fpwwe2lem7  10585  fpwwe2  10591  gchdju1  10604  pwfseqlem3  10608  pwfseqlem4a  10609  pwfseqlem4  10610  gchpwdom  10618  tskss  10706  inar1  10723  gruss  10744  gruurn  10746  ltsonq  10917  distrlem4pr  10974  sqgt0sr  11054  map2psrpr  11058  letric  11273  renegcli  11482  addid0  11596  mulge0b  12052  nnge1  12231  0mnnnnn0  12503  nn0lt2  12626  zneo  12646  uzind2  12656  fzind  12661  nn0ind-raph  12663  uzwo  12902  nn01to3  12932  zbtwnre  12937  rpnnen1lem5  12972  ledivge1le  13056  xrletri  13145  qsqueeze  13194  difreicc  13478  elfzmlbp  13634  difelfznle  13637  elfzodifsumelfzo  13727  ssfzo12  13755  elfzonelfzo  13765  flflp1  13807  fleqceilz  13854  modsumfzodifsn  13947  addmodlteq  13949  om2uzf1oi  13956  expnngt1  14244  facdiv  14290  facwordi  14292  bcpasc  14324  hashdom  14382  hashgt23el  14427  hashdmpropge2  14486  ccatsymb  14586  swrdnnn0nd  14660  swrdnd0  14661  swrdsbslen  14668  swrdspsleq  14669  swrdlsw  14671  pfxnd0  14692  swrdswrdlem  14707  swrdccatin1  14728  pfxccatin12lem3  14735  swrdccat  14738  pfxccat3a  14741  repswswrd  14787  cshwidx0  14809  cshwcsh2id  14831  limsupbnd1  15485  lo1bdd2  15527  addcn2  15597  mulcn2  15599  o1rlimmul  15622  lo1add  15630  lo1mul  15631  rlimno1  15657  ruclem3  16241  odd2np1  16351  oddge22np1  16359  bitsfzo  16445  cncongr1  16677  2mulprm  16703  prm23ge5  16827  pcdvdsb  16881  pcaddlem  16900  infpnlem1  16922  prmunb  16926  vdwlem9  17001  vdwnnlem3  17009  ramcl  17041  prmgaplem5  17067  cshwshash  17116  setcmon  18096  setcepi  18097  setciso  18100  xpsmnd0  18788  f1ghm0to0  19261  ghmf1  19262  sylow2alem2  19634  sylow2blem3  19638  qusabl  19881  lt6abl  19911  cyggexb  19915  gsumcom2  19991  ringurd  20207  imasring  20351  xpsring1d  20354  0ring1eq0  20555  subrgdvds  20608  rngciso  20660  ringciso  20694  isdomn4  20738  drnginvrcl  20775  drnginvrl  20778  drnginvrr  20779  lsmelval2  21125  quscrng  21326  xrsdsreclblem  21438  obs2ss  21754  obslbs  21755  rnasclassa  21920  mplsubrglem  22028  psdmul  22204  gsummoncoe1  22344  mp2pm2mplem4  22842  chfacfisf  22887  chfacfisfcpmat  22888  cayleyhamilton1  22925  cmpsublem  23432  cmpsub  23433  1stccnp  23495  locfincf  23564  txhaus  23680  xkohaus  23686  ufilss  23938  cfinufil  23961  fmfnfmlem1  23987  hausflim  24014  fclscf  24058  alexsubb  24079  qustgplem  24154  prdsbl  24524  metss2lem  24544  nghmcn  24778  cfil3i  25304  cmetcaulem  25323  minveclem4  25467  ovolgelb  25515  ovolunnul  25535  ovoliun  25540  ovoliunnul  25542  ovolicc2lem2  25553  iundisj2  25584  voliunlem3  25587  rolle  26025  dvlip  26028  lhop1lem  26048  lhop2  26050  dvfsumrlim  26066  deg1ge  26131  coeeulem  26257  dgrco  26308  radcnvlt1  26451  psercnlem1  26458  logcnlem2  26678  logcnlem3  26679  cxpeq  26792  angpined  26865  efrlim  27004  dmgmaddn0  27057  lgamucov  27072  basellem2  27116  ppieq0  27210  mumullem2  27214  chpeq0  27242  chteq0  27243  chtub  27246  fsumvma  27247  dchrptlem1  27298  bposlem6  27323  gausslemma2dlem0i  27398  gausslemma2dlem1a  27399  lgseisenlem2  27410  2sqlem6  27457  2sq2  27467  2sqnn0  27472  2sqreulem1  27480  2sqreunnlem1  27483  dchrisum0lem1  27550  pntrsumbnd2  27601  pntlem3  27643  noextenddif  27702  nosupno  27737  nosupbnd1  27748  noinfno  27752  noinfbnd1  27763  noetasuplem4  27770  noetainflem4  27774  cutsun12  27853  lesrec  27862  cutlt  27995  leadds2im  28051  oniso  28334  n0fincut  28418  bdayfinbndlem1  28530  z12bdaylem1  28533  colinearalg  29050  eengtrkg  29126  incistruhgr  29219  wlkv0  29789  crctcshwlkn0  29960  clwwlkccatlem  30130  clwlkclwwlklem2a4  30138  clwlkclwwlklem2  30141  clwlkclwwlkfo  30150  eucrctshift  30384  frrusgrord0  30481  frgrreg  30535  blocni  30947  ubthlem1  31012  minvecolem4  31022  shmodsi  31531  atcvati  32528  atcvat2i  32529  chirredlem4  32535  atmd2  32542  sumdmdlem  32560  addltmulALT  32588  iundisj2f  32732  iundisj2fi  32942  f1resveqaeq  35336  erdszelem9  35497  satffunlem1lem2  35701  satffunlem2lem2  35704  rdgprc  36090  cgrsub  36343  btwnxfr  36354  lineext  36374  linecgr  36379  btwnconn1lem4  36388  btwnconn1lem5  36389  btwnconn1lem6  36390  btwnconn1lem8  36392  btwnconn1lem11  36395  mh-inf3f1  36849  mptsnunlem  37780  finxpreclem6  37838  ltflcei  38055  poimirlem23  38090  poimirlem24  38091  poimirlem31  38098  poimirlem32  38099  ftc1anclem5  38144  heiborlem6  38263  grpokerinj  38340  dvrunz  38401  isdmn3  38521  dmncan1  38523  membpartlem19  39361  l1cvpat  39626  atnle  39889  cvlexch3  39904  cvlexch4N  39905  cvlatexchb1  39906  cvrat2  40001  atlelt  40010  3dimlem4a  40035  3dimlem4OLDN  40037  ps-1  40049  ps-2  40050  4atlem10  40178  4atlem11  40181  4atlem12  40184  cdleme11c  40833  cdleme21c  40899  cdlemg6d  41193  trlcoat  41295  tendoid0  41397  cdleml3N  41550  dia2dimlem7  41642  aks6d1c6lem3  42737  expeq1d  42881  fsuppind  43120  pellexlem1  43354  pellexlem6  43359  imasgim  43625  onsupmaxb  43764  safesnsupfidom1o  43941  reabsifnpos  44157  reabsifnneg  44159  iunrelexpmin1  44232  iunrelexpmin2  44236  radcnvrat  44838  nzss  44841  pwclaxpow  45508  ormkglobd  47399  elprneb  47571  or2expropbi  47576  tz6.12i-afv2  47785  dfatcolem  47797  f1oresf1o2  47833  zm1nn  47844  2ffzoeq  47870  modmkpkne  47909  sfprmdvdsmersenne  48160  lighneallem3  48164  lighneallem4  48167  requad01  48191  fppr2odd  48301  fpprwppr  48309  stgoldbwt  48346  sbgoldbaltlem1  48349  isuspgrimlem  48465  upgrimpthslem2  48478  isubgr3stgrlem4  48539  isubgr3stgrlem7  48542  gpg5nbgrvtx03starlem1  48638  gpg5nbgrvtx03starlem3  48640  gpg5nbgrvtx13starlem1  48641  gpg5nbgrvtx13starlem3  48643  lmod0rng  48799  lidldomn1  48801  rngcisoALTV  48847  ringcisoALTV  48881  ztprmneprm  48917  lincresunit3  49051  itsclc0yqsol  49334  itschlc0xyqsol1  49336  aacllem  50370