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  3665  eqreu  3751  sotr2  5641  sotr3  5648  sossfld  6217  ordintdif  6445  tz6.12i  6948  f1cofveqaeqALT  7296  soisoi  7364  riotaeqimp  7431  ov3  7613  tfindsg  7898  tfindsg2  7899  nnsuc  7921  findsg  7937  soseq  8200  suppssr  8236  suppssrg  8237  tfrlem9  8441  oe0lem  8569  oa00  8615  omwordi  8627  om00  8631  omass  8636  oelim2  8651  oeoa  8653  oeoe  8655  nnmwordi  8691  swoso  8797  dom2lem  9052  onsdominel  9192  f1finf1o  9333  f1finf1oOLD  9334  fiint  9394  cantnfp1lem3  9749  cantnfp1  9750  cantnflem1  9758  ttrclselem2  9795  rankr1ai  9867  rankval3b  9895  harcard  10047  infxpenlem  10082  alephnbtwn  10140  alephinit  10164  infxp  10283  cofsmo  10338  infpssALT  10382  fin23lem24  10391  fin56  10462  ttukeylem6  10583  ficard  10634  alephval2  10641  fpwwe2lem7  10706  fpwwe2  10712  gchdju1  10725  pwfseqlem3  10729  pwfseqlem4a  10730  pwfseqlem4  10731  gchpwdom  10739  tskss  10827  inar1  10844  gruss  10865  gruurn  10867  ltsonq  11038  distrlem4pr  11095  sqgt0sr  11175  map2psrpr  11179  letric  11390  renegcli  11597  addid0  11709  mulge0b  12165  nnge1  12321  0mnnnnn0  12585  nn0lt2  12706  zneo  12726  uzind2  12736  fzind  12741  nn0ind-raph  12743  uzwo  12976  nn01to3  13006  zbtwnre  13011  rpnnen1lem5  13046  ledivge1le  13128  xrletri  13215  qsqueeze  13263  difreicc  13544  elfzmlbp  13696  difelfznle  13699  elfzodifsumelfzo  13782  ssfzo12  13809  elfzonelfzo  13819  flflp1  13858  fleqceilz  13905  modsumfzodifsn  13995  addmodlteq  13997  om2uzf1oi  14004  expnngt1  14290  facdiv  14336  facwordi  14338  bcpasc  14370  hashdom  14428  hashgt23el  14473  hashdmpropge2  14532  ccatsymb  14630  swrdnnn0nd  14704  swrdnd0  14705  swrdsbslen  14712  swrdspsleq  14713  swrdlsw  14715  pfxnd0  14736  swrdswrdlem  14752  swrdccatin1  14773  pfxccatin12lem3  14780  swrdccat  14783  pfxccat3a  14786  repswswrd  14832  cshwidx0  14854  cshwcsh2id  14877  limsupbnd1  15528  lo1bdd2  15570  addcn2  15640  mulcn2  15642  o1rlimmul  15665  lo1add  15673  lo1mul  15674  rlimno1  15702  ruclem3  16281  odd2np1  16389  oddge22np1  16397  bitsfzo  16481  cncongr1  16714  2mulprm  16740  prm23ge5  16862  pcdvdsb  16916  pcaddlem  16935  infpnlem1  16957  prmunb  16961  vdwlem9  17036  vdwnnlem3  17044  ramcl  17076  prmgaplem5  17102  cshwshash  17152  setcmon  18154  setcepi  18155  setciso  18158  xpsmnd0  18813  f1ghm0to0  19285  ghmf1  19286  sylow2alem2  19660  sylow2blem3  19664  qusabl  19907  lt6abl  19937  cyggexb  19941  gsumcom2  20017  ringurd  20212  imasring  20353  xpsring1d  20356  0ring1eq0  20559  subrgdvds  20614  rngciso  20660  ringciso  20694  isdomn4  20738  drnginvrcl  20775  drnginvrl  20778  drnginvrr  20779  lsmelval2  21107  quscrng  21316  xrsdsreclblem  21453  obs2ss  21772  obslbs  21773  rnasclassa  21938  mplsubrglem  22047  psdmul  22193  gsummoncoe1  22333  mp2pm2mplem4  22836  chfacfisf  22881  chfacfisfcpmat  22882  cayleyhamilton1  22919  cmpsublem  23428  cmpsub  23429  1stccnp  23491  locfincf  23560  txhaus  23676  xkohaus  23682  ufilss  23934  cfinufil  23957  fmfnfmlem1  23983  hausflim  24010  fclscf  24054  alexsubb  24075  qustgplem  24150  prdsbl  24525  metss2lem  24545  nghmcn  24787  cfil3i  25322  cmetcaulem  25341  minveclem4  25485  ovolgelb  25534  ovolunnul  25554  ovoliun  25559  ovoliunnul  25561  ovolicc2lem2  25572  iundisj2  25603  voliunlem3  25606  rolle  26048  dvlip  26052  lhop1lem  26072  lhop2  26074  dvfsumrlim  26092  deg1ge  26157  coeeulem  26283  dgrco  26335  radcnvlt1  26479  psercnlem1  26487  logcnlem2  26703  logcnlem3  26704  cxpeq  26818  angpined  26891  efrlim  27030  efrlimOLD  27031  dmgmaddn0  27084  lgamucov  27099  basellem2  27143  ppieq0  27237  mumullem2  27241  chpeq0  27270  chteq0  27271  chtub  27274  fsumvma  27275  dchrptlem1  27326  bposlem6  27351  gausslemma2dlem0i  27426  gausslemma2dlem1a  27427  lgseisenlem2  27438  2sqlem6  27485  2sq2  27495  2sqnn0  27500  2sqreulem1  27508  2sqreunnlem1  27511  dchrisum0lem1  27578  pntrsumbnd2  27629  pntlem3  27671  noextenddif  27731  nosupno  27766  nosupbnd1  27777  noinfno  27781  noinfbnd1  27792  noetasuplem4  27799  noetainflem4  27803  scutun12  27873  slerec  27882  cutlt  27984  sleadd2im  28039  colinearalg  28943  eengtrkg  29019  incistruhgr  29114  wlkv0  29687  crctcshwlkn0  29854  clwwlkccatlem  30021  clwlkclwwlklem2a4  30029  clwlkclwwlklem2  30032  clwlkclwwlkfo  30041  eucrctshift  30275  frrusgrord0  30372  frgrreg  30426  blocni  30837  ubthlem1  30902  minvecolem4  30912  shmodsi  31421  atcvati  32418  atcvat2i  32419  chirredlem4  32425  atmd2  32432  sumdmdlem  32450  addltmulALT  32478  iundisj2f  32612  iundisj2fi  32802  f1resveqaeq  35061  erdszelem9  35167  satffunlem1lem2  35371  satffunlem2lem2  35374  rdgprc  35758  cgrsub  36009  btwnxfr  36020  lineext  36040  linecgr  36045  btwnconn1lem4  36054  btwnconn1lem5  36055  btwnconn1lem6  36056  btwnconn1lem8  36058  btwnconn1lem11  36061  mptsnunlem  37304  finxpreclem6  37362  ltflcei  37568  poimirlem23  37603  poimirlem24  37604  poimirlem31  37611  poimirlem32  37612  ftc1anclem5  37657  heiborlem6  37776  grpokerinj  37853  dvrunz  37914  isdmn3  38034  dmncan1  38036  membpartlem19  38767  l1cvpat  39010  atnle  39273  cvlexch3  39288  cvlexch4N  39289  cvlatexchb1  39290  cvrat2  39386  atlelt  39395  3dimlem4a  39420  3dimlem4OLDN  39422  ps-1  39434  ps-2  39435  4atlem10  39563  4atlem11  39566  4atlem12  39569  cdleme11c  40218  cdleme21c  40284  cdlemg6d  40578  trlcoat  40680  tendoid0  40782  cdleml3N  40935  dia2dimlem7  41027  aks6d1c6lem3  42129  metakunt1  42162  metakunt6  42167  expeq1d  42311  fsuppind  42545  pellexlem1  42785  pellexlem6  42790  imasgim  43057  onsupmaxb  43200  safesnsupfidom1o  43379  reabsifnpos  43595  reabsifnneg  43597  iunrelexpmin1  43670  iunrelexpmin2  43674  radcnvrat  44283  nzss  44286  elprneb  46944  or2expropbi  46949  tz6.12i-afv2  47158  dfatcolem  47170  f1oresf1o2  47206  zm1nn  47217  2ffzoeq  47242  sfprmdvdsmersenne  47477  lighneallem3  47481  lighneallem4  47484  requad01  47495  fppr2odd  47605  fpprwppr  47613  stgoldbwt  47650  sbgoldbaltlem1  47653  isuspgrimlem  47758  lmod0rng  47952  lidldomn1  47954  rngcisoALTV  48000  ringcisoALTV  48034  ztprmneprm  48072  lincresunit3  48210  itsclc0yqsol  48498  itschlc0xyqsol1  48500  aacllem  48895