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  3595  eqreu  3676  sotr2  5564  sotr3  5571  sossfld  6142  ordintdif  6366  tz6.12i  6858  f1cofveqaeqALT  7204  soisoi  7274  riotaeqimp  7341  ov3  7521  tfindsg  7803  tfindsg2  7804  nnsuc  7826  findsg  7839  soseq  8100  suppssr  8136  suppssrg  8137  tfrlem9  8315  oe0lem  8439  oa00  8485  omwordi  8497  om00  8501  omass  8506  oelim2  8522  oeoa  8524  oeoe  8526  nnmwordi  8562  swoso  8669  dom2lem  8930  onsdominel  9055  f1finf1o  9174  fiint  9228  cantnfp1lem3  9590  cantnfp1  9591  cantnflem1  9599  ttrclselem2  9636  rankr1ai  9711  rankval3b  9739  harcard  9891  infxpenlem  9924  alephnbtwn  9982  alephinit  10006  infxp  10125  cofsmo  10180  infpssALT  10224  fin23lem24  10233  fin56  10304  ttukeylem6  10425  ficard  10476  alephval2  10484  fpwwe2lem7  10549  fpwwe2  10555  gchdju1  10568  pwfseqlem3  10572  pwfseqlem4a  10573  pwfseqlem4  10574  gchpwdom  10582  tskss  10670  inar1  10687  gruss  10708  gruurn  10710  ltsonq  10881  distrlem4pr  10938  sqgt0sr  11018  map2psrpr  11022  letric  11235  renegcli  11444  addid0  11558  mulge0b  12015  nnge1  12194  0mnnnnn0  12458  nn0lt2  12581  zneo  12601  uzind2  12611  fzind  12616  nn0ind-raph  12618  uzwo  12850  nn01to3  12880  zbtwnre  12885  rpnnen1lem5  12920  ledivge1le  13004  xrletri  13093  qsqueeze  13142  difreicc  13426  elfzmlbp  13582  difelfznle  13585  elfzodifsumelfzo  13675  ssfzo12  13703  elfzonelfzo  13713  flflp1  13755  fleqceilz  13802  modsumfzodifsn  13895  addmodlteq  13897  om2uzf1oi  13904  expnngt1  14192  facdiv  14238  facwordi  14240  bcpasc  14272  hashdom  14330  hashgt23el  14375  hashdmpropge2  14434  ccatsymb  14534  swrdnnn0nd  14608  swrdnd0  14609  swrdsbslen  14616  swrdspsleq  14617  swrdlsw  14619  pfxnd0  14640  swrdswrdlem  14655  swrdccatin1  14676  pfxccatin12lem3  14683  swrdccat  14686  pfxccat3a  14689  repswswrd  14735  cshwidx0  14757  cshwcsh2id  14779  limsupbnd1  15433  lo1bdd2  15475  addcn2  15545  mulcn2  15547  o1rlimmul  15570  lo1add  15578  lo1mul  15579  rlimno1  15605  ruclem3  16189  odd2np1  16299  oddge22np1  16307  bitsfzo  16393  cncongr1  16625  2mulprm  16651  prm23ge5  16775  pcdvdsb  16829  pcaddlem  16848  infpnlem1  16870  prmunb  16874  vdwlem9  16949  vdwnnlem3  16957  ramcl  16989  prmgaplem5  17015  cshwshash  17064  setcmon  18043  setcepi  18044  setciso  18047  xpsmnd0  18735  f1ghm0to0  19209  ghmf1  19210  sylow2alem2  19582  sylow2blem3  19586  qusabl  19829  lt6abl  19859  cyggexb  19863  gsumcom2  19939  ringurd  20155  imasring  20299  xpsring1d  20302  0ring1eq0  20499  subrgdvds  20552  rngciso  20604  ringciso  20638  isdomn4  20682  drnginvrcl  20719  drnginvrl  20722  drnginvrr  20723  lsmelval2  21070  quscrng  21271  xrsdsreclblem  21400  obs2ss  21717  obslbs  21718  rnasclassa  21883  mplsubrglem  21991  psdmul  22141  gsummoncoe1  22282  mp2pm2mplem4  22783  chfacfisf  22828  chfacfisfcpmat  22829  cayleyhamilton1  22866  cmpsublem  23373  cmpsub  23374  1stccnp  23436  locfincf  23505  txhaus  23621  xkohaus  23627  ufilss  23879  cfinufil  23902  fmfnfmlem1  23928  hausflim  23955  fclscf  23999  alexsubb  24020  qustgplem  24095  prdsbl  24465  metss2lem  24485  nghmcn  24719  cfil3i  25245  cmetcaulem  25264  minveclem4  25408  ovolgelb  25456  ovolunnul  25476  ovoliun  25481  ovoliunnul  25483  ovolicc2lem2  25494  iundisj2  25525  voliunlem3  25528  rolle  25966  dvlip  25970  lhop1lem  25990  lhop2  25992  dvfsumrlim  26010  deg1ge  26075  coeeulem  26201  dgrco  26252  radcnvlt1  26398  psercnlem1  26406  logcnlem2  26623  logcnlem3  26624  cxpeq  26738  angpined  26811  efrlim  26950  efrlimOLD  26951  dmgmaddn0  27004  lgamucov  27019  basellem2  27063  ppieq0  27157  mumullem2  27161  chpeq0  27190  chteq0  27191  chtub  27194  fsumvma  27195  dchrptlem1  27246  bposlem6  27271  gausslemma2dlem0i  27346  gausslemma2dlem1a  27347  lgseisenlem2  27358  2sqlem6  27405  2sq2  27415  2sqnn0  27420  2sqreulem1  27428  2sqreunnlem1  27431  dchrisum0lem1  27498  pntrsumbnd2  27549  pntlem3  27591  noextenddif  27651  nosupno  27686  nosupbnd1  27697  noinfno  27701  noinfbnd1  27712  noetasuplem4  27719  noetainflem4  27723  cutsun12  27801  lesrec  27810  cutlt  27943  leadds2im  27999  oniso  28282  n0fincut  28366  bdayfinbndlem1  28478  z12bdaylem1  28481  colinearalg  28998  eengtrkg  29074  incistruhgr  29167  wlkv0  29738  crctcshwlkn0  29909  clwwlkccatlem  30079  clwlkclwwlklem2a4  30087  clwlkclwwlklem2  30090  clwlkclwwlkfo  30099  eucrctshift  30333  frrusgrord0  30430  frgrreg  30484  blocni  30896  ubthlem1  30961  minvecolem4  30971  shmodsi  31480  atcvati  32477  atcvat2i  32478  chirredlem4  32484  atmd2  32491  sumdmdlem  32509  addltmulALT  32537  iundisj2f  32680  iundisj2fi  32890  f1resveqaeq  35249  erdszelem9  35402  satffunlem1lem2  35606  satffunlem2lem2  35609  rdgprc  35995  cgrsub  36248  btwnxfr  36259  lineext  36279  linecgr  36284  btwnconn1lem4  36293  btwnconn1lem5  36294  btwnconn1lem6  36295  btwnconn1lem8  36297  btwnconn1lem11  36300  mptsnunlem  37665  finxpreclem6  37723  ltflcei  37940  poimirlem23  37975  poimirlem24  37976  poimirlem31  37983  poimirlem32  37984  ftc1anclem5  38029  heiborlem6  38148  grpokerinj  38225  dvrunz  38286  isdmn3  38406  dmncan1  38408  membpartlem19  39246  l1cvpat  39511  atnle  39774  cvlexch3  39789  cvlexch4N  39790  cvlatexchb1  39791  cvrat2  39886  atlelt  39895  3dimlem4a  39920  3dimlem4OLDN  39922  ps-1  39934  ps-2  39935  4atlem10  40063  4atlem11  40066  4atlem12  40069  cdleme11c  40718  cdleme21c  40784  cdlemg6d  41078  trlcoat  41180  tendoid0  41282  cdleml3N  41435  dia2dimlem7  41527  aks6d1c6lem3  42622  expeq1d  42767  fsuppind  43034  pellexlem1  43272  pellexlem6  43277  imasgim  43543  onsupmaxb  43682  safesnsupfidom1o  43859  reabsifnpos  44075  reabsifnneg  44077  iunrelexpmin1  44150  iunrelexpmin2  44154  radcnvrat  44756  nzss  44759  pwclaxpow  45426  ormkglobd  47318  elprneb  47474  or2expropbi  47479  tz6.12i-afv2  47688  dfatcolem  47700  f1oresf1o2  47736  zm1nn  47747  2ffzoeq  47773  modmkpkne  47812  sfprmdvdsmersenne  48063  lighneallem3  48067  lighneallem4  48070  requad01  48094  fppr2odd  48204  fpprwppr  48212  stgoldbwt  48249  sbgoldbaltlem1  48252  isuspgrimlem  48368  upgrimpthslem2  48381  isubgr3stgrlem4  48442  isubgr3stgrlem7  48445  gpg5nbgrvtx03starlem1  48541  gpg5nbgrvtx03starlem3  48543  gpg5nbgrvtx13starlem1  48544  gpg5nbgrvtx13starlem3  48546  lmod0rng  48702  lidldomn1  48704  rngcisoALTV  48750  ringcisoALTV  48784  ztprmneprm  48820  lincresunit3  48954  itsclc0yqsol  49237  itschlc0xyqsol1  49239  aacllem  50273