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 205

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 206

This theorem is referenced by:  3imtr3d  293  ceqex  3587  eqreu  3669  sotr2  5546  sossfld  6104  ordintdif  6330  tz6.12i  6832  f1cofveqaeqALT  7164  soisoi  7231  riotaeqimp  7291  ov3  7467  tfindsg  7739  tfindsg2  7740  nnsuc  7762  findsg  7778  suppssr  8043  suppssrg  8044  tfrlem9  8247  oe0lem  8374  oa00  8421  omwordi  8433  om00  8437  omass  8442  oelim2  8457  oeoa  8459  oeoe  8461  nnmwordi  8497  swoso  8562  dom2lem  8813  onsdominel  8951  f1finf1o  9090  cantnfp1lem3  9482  cantnfp1  9483  cantnflem1  9491  ttrclselem2  9528  rankr1ai  9600  rankval3b  9628  harcard  9780  infxpenlem  9815  alephnbtwn  9873  alephinit  9897  infxp  10017  cofsmo  10071  infpssALT  10115  fin23lem24  10124  fin56  10195  ttukeylem6  10316  ficard  10367  alephval2  10374  fpwwe2lem7  10439  fpwwe2  10445  gchdju1  10458  pwfseqlem3  10462  pwfseqlem4a  10463  pwfseqlem4  10464  gchpwdom  10472  tskss  10560  inar1  10577  gruss  10598  gruurn  10600  ltsonq  10771  distrlem4pr  10828  sqgt0sr  10908  map2psrpr  10912  letric  11121  renegcli  11328  addid0  11440  mulge0b  11891  nnge1  12047  0mnnnnn0  12311  nn0lt2  12429  zneo  12449  uzind2  12459  fzind  12464  nn0ind-raph  12466  uzwo  12697  nn01to3  12727  zbtwnre  12732  rpnnen1lem5  12767  ledivge1le  12847  xrletri  12933  qsqueeze  12981  difreicc  13262  elfzmlbp  13413  difelfznle  13416  elfzodifsumelfzo  13499  ssfzo12  13526  elfzonelfzo  13535  flflp1  13573  fleqceilz  13620  modsumfzodifsn  13710  addmodlteq  13712  om2uzf1oi  13719  expnngt1  14002  facdiv  14047  facwordi  14049  bcpasc  14081  hashdom  14139  hashgt23el  14184  hashdmpropge2  14242  ccatsymb  14332  swrdnnn0nd  14414  swrdnd0  14415  swrdsbslen  14422  swrdspsleq  14423  swrdlsw  14425  pfxnd0  14446  swrdswrdlem  14462  swrdccatin1  14483  pfxccatin12lem3  14490  swrdccat  14493  pfxccat3a  14496  repswswrd  14542  cshwidx0  14564  cshwcsh2id  14586  limsupbnd1  15236  lo1bdd2  15278  addcn2  15348  mulcn2  15350  o1rlimmul  15373  lo1add  15381  lo1mul  15382  rlimno1  15410  ruclem3  15987  odd2np1  16095  oddge22np1  16103  bitsfzo  16187  cncongr1  16417  2mulprm  16443  prm23ge5  16561  pcdvdsb  16615  pcaddlem  16634  infpnlem1  16656  prmunb  16660  vdwlem9  16735  vdwnnlem3  16743  ramcl  16775  prmgaplem5  16801  cshwshash  16851  setcmon  17847  setcepi  17848  setciso  17851  ghmf1  18908  sylow2alem2  19268  sylow2blem3  19272  qusabl  19511  lt6abl  19541  cyggexb  19545  gsumcom2  19621  imasring  19903  f1ghm0to0  20029  drnginvrcl  20053  drnginvrl  20055  drnginvrr  20056  subrgdvds  20083  lsmelval2  20392  quscrng  20556  xrsdsreclblem  20689  obs2ss  20981  obslbs  20982  rnasclassa  21144  mplsubrglem  21255  gsummoncoe1  21520  mp2pm2mplem4  22003  chfacfisf  22048  chfacfisfcpmat  22049  cayleyhamilton1  22086  cmpsublem  22595  cmpsub  22596  1stccnp  22658  locfincf  22727  txhaus  22843  xkohaus  22849  ufilss  23101  cfinufil  23124  fmfnfmlem1  23150  hausflim  23177  fclscf  23221  alexsubb  23242  qustgplem  23317  prdsbl  23692  metss2lem  23712  nghmcn  23954  cfil3i  24478  cmetcaulem  24497  minveclem4  24641  ovolgelb  24689  ovolunnul  24709  ovoliun  24714  ovoliunnul  24716  ovolicc2lem2  24727  iundisj2  24758  voliunlem3  24761  rolle  25199  dvlip  25202  lhop1lem  25222  lhop2  25224  dvfsumrlim  25240  deg1ge  25308  coeeulem  25430  dgrco  25481  radcnvlt1  25622  psercnlem1  25629  logcnlem2  25843  logcnlem3  25844  cxpeq  25955  angpined  26025  efrlim  26164  dmgmaddn0  26217  lgamucov  26232  basellem2  26276  ppieq0  26370  mumullem2  26374  chpeq0  26401  chteq0  26402  chtub  26405  fsumvma  26406  dchrptlem1  26457  bposlem6  26482  gausslemma2dlem0i  26557  gausslemma2dlem1a  26558  lgseisenlem2  26569  2sqlem6  26616  2sq2  26626  2sqnn0  26631  2sqreulem1  26639  2sqreunnlem1  26642  dchrisum0lem1  26709  pntrsumbnd2  26760  pntlem3  26802  colinearalg  27323  eengtrkg  27399  incistruhgr  27494  wlkv0  28063  crctcshwlkn0  28231  clwwlkccatlem  28398  clwlkclwwlklem2a4  28406  clwlkclwwlklem2  28409  clwlkclwwlkfo  28418  eucrctshift  28652  frrusgrord0  28749  frgrreg  28803  blocni  29212  ubthlem1  29277  minvecolem4  29287  shmodsi  29796  atcvati  30793  atcvat2i  30794  chirredlem4  30800  atmd2  30807  sumdmdlem  30825  addltmulALT  30853  iundisj2f  30974  iundisj2fi  31163  rngurd  31527  f1resveqaeq  33102  erdszelem9  33206  satffunlem1lem2  33410  satffunlem2lem2  33413  sotr3  33778  rdgprc  33815  soseq  33848  noextenddif  33916  nosupno  33951  nosupbnd1  33962  noinfno  33966  noinfbnd1  33977  noetasuplem4  33984  noetainflem4  33988  scutun12  34049  slerec  34058  cgrsub  34392  btwnxfr  34403  lineext  34423  linecgr  34428  btwnconn1lem4  34437  btwnconn1lem5  34438  btwnconn1lem6  34439  btwnconn1lem8  34441  btwnconn1lem11  34444  mptsnunlem  35553  finxpreclem6  35611  ltflcei  35809  poimirlem23  35844  poimirlem24  35845  poimirlem31  35852  poimirlem32  35853  ftc1anclem5  35898  heiborlem6  36018  grpokerinj  36095  dvrunz  36156  isdmn3  36276  dmncan1  36278  l1cvpat  37110  atnle  37373  cvlexch3  37388  cvlexch4N  37389  cvlatexchb1  37390  cvrat2  37485  atlelt  37494  3dimlem4a  37519  3dimlem4OLDN  37521  ps-1  37533  ps-2  37534  4atlem10  37662  4atlem11  37665  4atlem12  37668  cdleme11c  38317  cdleme21c  38383  cdlemg6d  38677  trlcoat  38779  tendoid0  38881  cdleml3N  39034  dia2dimlem7  39126  metakunt1  40167  metakunt6  40172  isdomn4  40214  fsuppind  40316  pellexlem1  40688  pellexlem6  40693  imasgim  40963  reabsifnpos  41279  reabsifnneg  41281  iunrelexpmin1  41354  iunrelexpmin2  41358  radcnvrat  41970  nzss  41973  elprneb  44581  or2expropbi  44586  tz6.12i-afv2  44793  dfatcolem  44805  f1oresf1o2  44841  zm1nn  44852  2ffzoeq  44878  sfprmdvdsmersenne  45113  lighneallem3  45117  lighneallem4  45120  requad01  45131  fppr2odd  45241  fpprwppr  45249  stgoldbwt  45286  sbgoldbaltlem1  45289  isomuspgrlem1  45337  lmod0rng  45484  0ring1eq0  45488  lidldomn1  45537  rngciso  45598  rngcisoALTV  45610  ringciso  45649  ringcisoALTV  45673  ztprmneprm  45741  lincresunit3  45880  itsclc0yqsol  46168  itschlc0xyqsol1  46170  aacllem  46563