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  3607  eqreu  3688  sotr2  5567  sotr3  5574  sossfld  6145  ordintdif  6369  tz6.12i  6861  f1cofveqaeqALT  7206  soisoi  7276  riotaeqimp  7343  ov3  7523  tfindsg  7805  tfindsg2  7806  nnsuc  7828  findsg  7841  soseq  8103  suppssr  8139  suppssrg  8140  tfrlem9  8318  oe0lem  8442  oa00  8488  omwordi  8500  om00  8504  omass  8509  oelim2  8525  oeoa  8527  oeoe  8529  nnmwordi  8565  swoso  8672  dom2lem  8933  onsdominel  9058  f1finf1o  9177  fiint  9231  cantnfp1lem3  9593  cantnfp1  9594  cantnflem1  9602  ttrclselem2  9639  rankr1ai  9714  rankval3b  9742  harcard  9894  infxpenlem  9927  alephnbtwn  9985  alephinit  10009  infxp  10128  cofsmo  10183  infpssALT  10227  fin23lem24  10236  fin56  10307  ttukeylem6  10428  ficard  10479  alephval2  10487  fpwwe2lem7  10552  fpwwe2  10558  gchdju1  10571  pwfseqlem3  10575  pwfseqlem4a  10576  pwfseqlem4  10577  gchpwdom  10585  tskss  10673  inar1  10690  gruss  10711  gruurn  10713  ltsonq  10884  distrlem4pr  10941  sqgt0sr  11021  map2psrpr  11025  letric  11237  renegcli  11446  addid0  11560  mulge0b  12016  nnge1  12177  0mnnnnn0  12437  nn0lt2  12559  zneo  12579  uzind2  12589  fzind  12594  nn0ind-raph  12596  uzwo  12828  nn01to3  12858  zbtwnre  12863  rpnnen1lem5  12898  ledivge1le  12982  xrletri  13071  qsqueeze  13120  difreicc  13404  elfzmlbp  13559  difelfznle  13562  elfzodifsumelfzo  13651  ssfzo12  13679  elfzonelfzo  13689  flflp1  13731  fleqceilz  13778  modsumfzodifsn  13871  addmodlteq  13873  om2uzf1oi  13880  expnngt1  14168  facdiv  14214  facwordi  14216  bcpasc  14248  hashdom  14306  hashgt23el  14351  hashdmpropge2  14410  ccatsymb  14510  swrdnnn0nd  14584  swrdnd0  14585  swrdsbslen  14592  swrdspsleq  14593  swrdlsw  14595  pfxnd0  14616  swrdswrdlem  14631  swrdccatin1  14652  pfxccatin12lem3  14659  swrdccat  14662  pfxccat3a  14665  repswswrd  14711  cshwidx0  14733  cshwcsh2id  14755  limsupbnd1  15409  lo1bdd2  15451  addcn2  15521  mulcn2  15523  o1rlimmul  15546  lo1add  15554  lo1mul  15555  rlimno1  15581  ruclem3  16162  odd2np1  16272  oddge22np1  16280  bitsfzo  16366  cncongr1  16598  2mulprm  16624  prm23ge5  16747  pcdvdsb  16801  pcaddlem  16820  infpnlem1  16842  prmunb  16846  vdwlem9  16921  vdwnnlem3  16929  ramcl  16961  prmgaplem5  16987  cshwshash  17036  setcmon  18015  setcepi  18016  setciso  18019  xpsmnd0  18707  f1ghm0to0  19178  ghmf1  19179  sylow2alem2  19551  sylow2blem3  19555  qusabl  19798  lt6abl  19828  cyggexb  19832  gsumcom2  19908  ringurd  20124  imasring  20270  xpsring1d  20273  0ring1eq0  20470  subrgdvds  20523  rngciso  20575  ringciso  20609  isdomn4  20653  drnginvrcl  20690  drnginvrl  20693  drnginvrr  20694  lsmelval2  21041  quscrng  21242  xrsdsreclblem  21371  obs2ss  21688  obslbs  21689  rnasclassa  21855  mplsubrglem  21963  psdmul  22113  gsummoncoe1  22256  mp2pm2mplem4  22757  chfacfisf  22802  chfacfisfcpmat  22803  cayleyhamilton1  22840  cmpsublem  23347  cmpsub  23348  1stccnp  23410  locfincf  23479  txhaus  23595  xkohaus  23601  ufilss  23853  cfinufil  23876  fmfnfmlem1  23902  hausflim  23929  fclscf  23973  alexsubb  23994  qustgplem  24069  prdsbl  24439  metss2lem  24459  nghmcn  24693  cfil3i  25229  cmetcaulem  25248  minveclem4  25392  ovolgelb  25441  ovolunnul  25461  ovoliun  25466  ovoliunnul  25468  ovolicc2lem2  25479  iundisj2  25510  voliunlem3  25513  rolle  25954  dvlip  25958  lhop1lem  25978  lhop2  25980  dvfsumrlim  25998  deg1ge  26063  coeeulem  26189  dgrco  26241  radcnvlt1  26387  psercnlem1  26395  logcnlem2  26612  logcnlem3  26613  cxpeq  26727  angpined  26800  efrlim  26939  efrlimOLD  26940  dmgmaddn0  26993  lgamucov  27008  basellem2  27052  ppieq0  27146  mumullem2  27150  chpeq0  27179  chteq0  27180  chtub  27183  fsumvma  27184  dchrptlem1  27235  bposlem6  27260  gausslemma2dlem0i  27335  gausslemma2dlem1a  27336  lgseisenlem2  27347  2sqlem6  27394  2sq2  27404  2sqnn0  27409  2sqreulem1  27417  2sqreunnlem1  27420  dchrisum0lem1  27487  pntrsumbnd2  27538  pntlem3  27580  noextenddif  27640  nosupno  27675  nosupbnd1  27686  noinfno  27690  noinfbnd1  27701  noetasuplem4  27708  noetainflem4  27712  scutun12  27788  slerec  27797  cutlt  27914  sleadd2im  27970  onsiso  28252  n0sfincut  28335  bdayfinbndlem1  28446  zs12bdaylem1  28449  colinearalg  28966  eengtrkg  29042  incistruhgr  29135  wlkv0  29706  crctcshwlkn0  29877  clwwlkccatlem  30047  clwlkclwwlklem2a4  30055  clwlkclwwlklem2  30058  clwlkclwwlkfo  30067  eucrctshift  30301  frrusgrord0  30398  frgrreg  30452  blocni  30863  ubthlem1  30928  minvecolem4  30938  shmodsi  31447  atcvati  32444  atcvat2i  32445  chirredlem4  32451  atmd2  32458  sumdmdlem  32476  addltmulALT  32504  iundisj2f  32647  iundisj2fi  32858  f1resveqaeq  35222  erdszelem9  35374  satffunlem1lem2  35578  satffunlem2lem2  35581  rdgprc  35967  cgrsub  36220  btwnxfr  36231  lineext  36251  linecgr  36256  btwnconn1lem4  36265  btwnconn1lem5  36266  btwnconn1lem6  36267  btwnconn1lem8  36269  btwnconn1lem11  36272  mptsnunlem  37514  finxpreclem6  37572  ltflcei  37780  poimirlem23  37815  poimirlem24  37816  poimirlem31  37823  poimirlem32  37824  ftc1anclem5  37869  heiborlem6  37988  grpokerinj  38065  dvrunz  38126  isdmn3  38246  dmncan1  38248  membpartlem19  39086  l1cvpat  39351  atnle  39614  cvlexch3  39629  cvlexch4N  39630  cvlatexchb1  39631  cvrat2  39726  atlelt  39735  3dimlem4a  39760  3dimlem4OLDN  39762  ps-1  39774  ps-2  39775  4atlem10  39903  4atlem11  39906  4atlem12  39909  cdleme11c  40558  cdleme21c  40624  cdlemg6d  40918  trlcoat  41020  tendoid0  41122  cdleml3N  41275  dia2dimlem7  41367  aks6d1c6lem3  42463  expeq1d  42615  fsuppind  42869  pellexlem1  43107  pellexlem6  43112  imasgim  43378  onsupmaxb  43517  safesnsupfidom1o  43694  reabsifnpos  43910  reabsifnneg  43912  iunrelexpmin1  43985  iunrelexpmin2  43989  radcnvrat  44591  nzss  44594  pwclaxpow  45261  ormkglobd  47155  elprneb  47311  or2expropbi  47316  tz6.12i-afv2  47525  dfatcolem  47537  f1oresf1o2  47573  zm1nn  47584  2ffzoeq  47609  modmkpkne  47643  sfprmdvdsmersenne  47885  lighneallem3  47889  lighneallem4  47892  requad01  47903  fppr2odd  48013  fpprwppr  48021  stgoldbwt  48058  sbgoldbaltlem1  48061  isuspgrimlem  48177  upgrimpthslem2  48190  isubgr3stgrlem4  48251  isubgr3stgrlem7  48254  gpg5nbgrvtx03starlem1  48350  gpg5nbgrvtx03starlem3  48352  gpg5nbgrvtx13starlem1  48353  gpg5nbgrvtx13starlem3  48355  lmod0rng  48511  lidldomn1  48513  rngcisoALTV  48559  ringcisoALTV  48593  ztprmneprm  48629  lincresunit3  48763  itsclc0yqsol  49046  itschlc0xyqsol1  49048  aacllem  50082