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  3608  eqreu  3689  sotr2  5574  sotr3  5581  sossfld  6152  ordintdif  6376  tz6.12i  6868  f1cofveqaeqALT  7214  soisoi  7284  riotaeqimp  7351  ov3  7531  tfindsg  7813  tfindsg2  7814  nnsuc  7836  findsg  7849  soseq  8111  suppssr  8147  suppssrg  8148  tfrlem9  8326  oe0lem  8450  oa00  8496  omwordi  8508  om00  8512  omass  8517  oelim2  8533  oeoa  8535  oeoe  8537  nnmwordi  8573  swoso  8680  dom2lem  8941  onsdominel  9066  f1finf1o  9185  fiint  9239  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  11245  renegcli  11454  addid0  11568  mulge0b  12024  nnge1  12185  0mnnnnn0  12445  nn0lt2  12567  zneo  12587  uzind2  12597  fzind  12602  nn0ind-raph  12604  uzwo  12836  nn01to3  12866  zbtwnre  12871  rpnnen1lem5  12906  ledivge1le  12990  xrletri  13079  qsqueeze  13128  difreicc  13412  elfzmlbp  13567  difelfznle  13570  elfzodifsumelfzo  13659  ssfzo12  13687  elfzonelfzo  13697  flflp1  13739  fleqceilz  13786  modsumfzodifsn  13879  addmodlteq  13881  om2uzf1oi  13888  expnngt1  14176  facdiv  14222  facwordi  14224  bcpasc  14256  hashdom  14314  hashgt23el  14359  hashdmpropge2  14418  ccatsymb  14518  swrdnnn0nd  14592  swrdnd0  14593  swrdsbslen  14600  swrdspsleq  14601  swrdlsw  14603  pfxnd0  14624  swrdswrdlem  14639  swrdccatin1  14660  pfxccatin12lem3  14667  swrdccat  14670  pfxccat3a  14673  repswswrd  14719  cshwidx0  14741  cshwcsh2id  14763  limsupbnd1  15417  lo1bdd2  15459  addcn2  15529  mulcn2  15531  o1rlimmul  15554  lo1add  15562  lo1mul  15563  rlimno1  15589  ruclem3  16170  odd2np1  16280  oddge22np1  16288  bitsfzo  16374  cncongr1  16606  2mulprm  16632  prm23ge5  16755  pcdvdsb  16809  pcaddlem  16828  infpnlem1  16850  prmunb  16854  vdwlem9  16929  vdwnnlem3  16937  ramcl  16969  prmgaplem5  16995  cshwshash  17044  setcmon  18023  setcepi  18024  setciso  18027  xpsmnd0  18715  f1ghm0to0  19186  ghmf1  19187  sylow2alem2  19559  sylow2blem3  19563  qusabl  19806  lt6abl  19836  cyggexb  19840  gsumcom2  19916  ringurd  20132  imasring  20278  xpsring1d  20281  0ring1eq0  20478  subrgdvds  20531  rngciso  20583  ringciso  20617  isdomn4  20661  drnginvrcl  20698  drnginvrl  20701  drnginvrr  20702  lsmelval2  21049  quscrng  21250  xrsdsreclblem  21379  obs2ss  21696  obslbs  21697  rnasclassa  21863  mplsubrglem  21971  psdmul  22121  gsummoncoe1  22264  mp2pm2mplem4  22765  chfacfisf  22810  chfacfisfcpmat  22811  cayleyhamilton1  22848  cmpsublem  23355  cmpsub  23356  1stccnp  23418  locfincf  23487  txhaus  23603  xkohaus  23609  ufilss  23861  cfinufil  23884  fmfnfmlem1  23910  hausflim  23937  fclscf  23981  alexsubb  24002  qustgplem  24077  prdsbl  24447  metss2lem  24467  nghmcn  24701  cfil3i  25237  cmetcaulem  25256  minveclem4  25400  ovolgelb  25449  ovolunnul  25469  ovoliun  25474  ovoliunnul  25476  ovolicc2lem2  25487  iundisj2  25518  voliunlem3  25521  rolle  25962  dvlip  25966  lhop1lem  25986  lhop2  25988  dvfsumrlim  26006  deg1ge  26071  coeeulem  26197  dgrco  26249  radcnvlt1  26395  psercnlem1  26403  logcnlem2  26620  logcnlem3  26621  cxpeq  26735  angpined  26808  efrlim  26947  efrlimOLD  26948  dmgmaddn0  27001  lgamucov  27016  basellem2  27060  ppieq0  27154  mumullem2  27158  chpeq0  27187  chteq0  27188  chtub  27191  fsumvma  27192  dchrptlem1  27243  bposlem6  27268  gausslemma2dlem0i  27343  gausslemma2dlem1a  27344  lgseisenlem2  27355  2sqlem6  27402  2sq2  27412  2sqnn0  27417  2sqreulem1  27425  2sqreunnlem1  27428  dchrisum0lem1  27495  pntrsumbnd2  27546  pntlem3  27588  noextenddif  27648  nosupno  27683  nosupbnd1  27694  noinfno  27698  noinfbnd1  27709  noetasuplem4  27716  noetainflem4  27720  cutsun12  27798  lesrec  27807  cutlt  27940  leadds2im  27996  oniso  28279  n0fincut  28363  bdayfinbndlem1  28475  z12bdaylem1  28478  colinearalg  28995  eengtrkg  29071  incistruhgr  29164  wlkv0  29735  crctcshwlkn0  29906  clwwlkccatlem  30076  clwlkclwwlklem2a4  30084  clwlkclwwlklem2  30087  clwlkclwwlkfo  30096  eucrctshift  30330  frrusgrord0  30427  frgrreg  30481  blocni  30892  ubthlem1  30957  minvecolem4  30967  shmodsi  31476  atcvati  32473  atcvat2i  32474  chirredlem4  32480  atmd2  32487  sumdmdlem  32505  addltmulALT  32533  iundisj2f  32676  iundisj2fi  32887  f1resveqaeq  35260  erdszelem9  35412  satffunlem1lem2  35616  satffunlem2lem2  35619  rdgprc  36005  cgrsub  36258  btwnxfr  36269  lineext  36289  linecgr  36294  btwnconn1lem4  36303  btwnconn1lem5  36304  btwnconn1lem6  36305  btwnconn1lem8  36307  btwnconn1lem11  36310  mptsnunlem  37582  finxpreclem6  37640  ltflcei  37848  poimirlem23  37883  poimirlem24  37884  poimirlem31  37891  poimirlem32  37892  ftc1anclem5  37937  heiborlem6  38056  grpokerinj  38133  dvrunz  38194  isdmn3  38314  dmncan1  38316  membpartlem19  39154  l1cvpat  39419  atnle  39682  cvlexch3  39697  cvlexch4N  39698  cvlatexchb1  39699  cvrat2  39794  atlelt  39803  3dimlem4a  39828  3dimlem4OLDN  39830  ps-1  39842  ps-2  39843  4atlem10  39971  4atlem11  39974  4atlem12  39977  cdleme11c  40626  cdleme21c  40692  cdlemg6d  40986  trlcoat  41088  tendoid0  41190  cdleml3N  41343  dia2dimlem7  41435  aks6d1c6lem3  42531  expeq1d  42683  fsuppind  42937  pellexlem1  43175  pellexlem6  43180  imasgim  43446  onsupmaxb  43585  safesnsupfidom1o  43762  reabsifnpos  43978  reabsifnneg  43980  iunrelexpmin1  44053  iunrelexpmin2  44057  radcnvrat  44659  nzss  44662  pwclaxpow  45329  ormkglobd  47222  elprneb  47378  or2expropbi  47383  tz6.12i-afv2  47592  dfatcolem  47604  f1oresf1o2  47640  zm1nn  47651  2ffzoeq  47676  modmkpkne  47710  sfprmdvdsmersenne  47952  lighneallem3  47956  lighneallem4  47959  requad01  47970  fppr2odd  48080  fpprwppr  48088  stgoldbwt  48125  sbgoldbaltlem1  48128  isuspgrimlem  48244  upgrimpthslem2  48257  isubgr3stgrlem4  48318  isubgr3stgrlem7  48321  gpg5nbgrvtx03starlem1  48417  gpg5nbgrvtx03starlem3  48419  gpg5nbgrvtx13starlem1  48420  gpg5nbgrvtx13starlem3  48422  lmod0rng  48578  lidldomn1  48580  rngcisoALTV  48626  ringcisoALTV  48660  ztprmneprm  48696  lincresunit3  48830  itsclc0yqsol  49113  itschlc0xyqsol1  49115  aacllem  50149