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  3605  eqreu  3686  sotr2  5556  sotr3  5563  sossfld  6130  ordintdif  6353  tz6.12i  6843  f1cofveqaeqALT  7187  soisoi  7257  riotaeqimp  7324  ov3  7504  tfindsg  7786  tfindsg2  7787  nnsuc  7809  findsg  7822  soseq  8084  suppssr  8120  suppssrg  8121  tfrlem9  8299  oe0lem  8423  oa00  8469  omwordi  8481  om00  8485  omass  8490  oelim2  8505  oeoa  8507  oeoe  8509  nnmwordi  8545  swoso  8651  dom2lem  8909  onsdominel  9034  f1finf1o  9152  fiint  9206  cantnfp1lem3  9565  cantnfp1  9566  cantnflem1  9574  ttrclselem2  9611  rankr1ai  9683  rankval3b  9711  harcard  9863  infxpenlem  9896  alephnbtwn  9954  alephinit  9978  infxp  10097  cofsmo  10152  infpssALT  10196  fin23lem24  10205  fin56  10276  ttukeylem6  10397  ficard  10448  alephval2  10455  fpwwe2lem7  10520  fpwwe2  10526  gchdju1  10539  pwfseqlem3  10543  pwfseqlem4a  10544  pwfseqlem4  10545  gchpwdom  10553  tskss  10641  inar1  10658  gruss  10679  gruurn  10681  ltsonq  10852  distrlem4pr  10909  sqgt0sr  10989  map2psrpr  10993  letric  11205  renegcli  11414  addid0  11528  mulge0b  11984  nnge1  12145  0mnnnnn0  12405  nn0lt2  12528  zneo  12548  uzind2  12558  fzind  12563  nn0ind-raph  12565  uzwo  12801  nn01to3  12831  zbtwnre  12836  rpnnen1lem5  12871  ledivge1le  12955  xrletri  13044  qsqueeze  13092  difreicc  13376  elfzmlbp  13531  difelfznle  13534  elfzodifsumelfzo  13623  ssfzo12  13651  elfzonelfzo  13661  flflp1  13703  fleqceilz  13750  modsumfzodifsn  13843  addmodlteq  13845  om2uzf1oi  13852  expnngt1  14140  facdiv  14186  facwordi  14188  bcpasc  14220  hashdom  14278  hashgt23el  14323  hashdmpropge2  14382  ccatsymb  14482  swrdnnn0nd  14556  swrdnd0  14557  swrdsbslen  14564  swrdspsleq  14565  swrdlsw  14567  pfxnd0  14588  swrdswrdlem  14603  swrdccatin1  14624  pfxccatin12lem3  14631  swrdccat  14634  pfxccat3a  14637  repswswrd  14683  cshwidx0  14705  cshwcsh2id  14727  limsupbnd1  15381  lo1bdd2  15423  addcn2  15493  mulcn2  15495  o1rlimmul  15518  lo1add  15526  lo1mul  15527  rlimno1  15553  ruclem3  16134  odd2np1  16244  oddge22np1  16252  bitsfzo  16338  cncongr1  16570  2mulprm  16596  prm23ge5  16719  pcdvdsb  16773  pcaddlem  16792  infpnlem1  16814  prmunb  16818  vdwlem9  16893  vdwnnlem3  16901  ramcl  16933  prmgaplem5  16959  cshwshash  17008  setcmon  17986  setcepi  17987  setciso  17990  xpsmnd0  18678  f1ghm0to0  19150  ghmf1  19151  sylow2alem2  19523  sylow2blem3  19527  qusabl  19770  lt6abl  19800  cyggexb  19804  gsumcom2  19880  ringurd  20096  imasring  20241  xpsring1d  20244  0ring1eq0  20441  subrgdvds  20494  rngciso  20546  ringciso  20580  isdomn4  20624  drnginvrcl  20661  drnginvrl  20664  drnginvrr  20665  lsmelval2  21012  quscrng  21213  xrsdsreclblem  21342  obs2ss  21659  obslbs  21660  rnasclassa  21825  mplsubrglem  21934  psdmul  22074  gsummoncoe1  22216  mp2pm2mplem4  22717  chfacfisf  22762  chfacfisfcpmat  22763  cayleyhamilton1  22800  cmpsublem  23307  cmpsub  23308  1stccnp  23370  locfincf  23439  txhaus  23555  xkohaus  23561  ufilss  23813  cfinufil  23836  fmfnfmlem1  23862  hausflim  23889  fclscf  23933  alexsubb  23954  qustgplem  24029  prdsbl  24399  metss2lem  24419  nghmcn  24653  cfil3i  25189  cmetcaulem  25208  minveclem4  25352  ovolgelb  25401  ovolunnul  25421  ovoliun  25426  ovoliunnul  25428  ovolicc2lem2  25439  iundisj2  25470  voliunlem3  25473  rolle  25914  dvlip  25918  lhop1lem  25938  lhop2  25940  dvfsumrlim  25958  deg1ge  26023  coeeulem  26149  dgrco  26201  radcnvlt1  26347  psercnlem1  26355  logcnlem2  26572  logcnlem3  26573  cxpeq  26687  angpined  26760  efrlim  26899  efrlimOLD  26900  dmgmaddn0  26953  lgamucov  26968  basellem2  27012  ppieq0  27106  mumullem2  27110  chpeq0  27139  chteq0  27140  chtub  27143  fsumvma  27144  dchrptlem1  27195  bposlem6  27220  gausslemma2dlem0i  27295  gausslemma2dlem1a  27296  lgseisenlem2  27307  2sqlem6  27354  2sq2  27364  2sqnn0  27369  2sqreulem1  27377  2sqreunnlem1  27380  dchrisum0lem1  27447  pntrsumbnd2  27498  pntlem3  27540  noextenddif  27600  nosupno  27635  nosupbnd1  27646  noinfno  27650  noinfbnd1  27661  noetasuplem4  27668  noetainflem4  27672  scutun12  27744  slerec  27753  cutlt  27869  sleadd2im  27924  onsiso  28198  n0sfincut  28275  colinearalg  28881  eengtrkg  28957  incistruhgr  29050  wlkv0  29621  crctcshwlkn0  29792  clwwlkccatlem  29959  clwlkclwwlklem2a4  29967  clwlkclwwlklem2  29970  clwlkclwwlkfo  29979  eucrctshift  30213  frrusgrord0  30310  frgrreg  30364  blocni  30775  ubthlem1  30840  minvecolem4  30850  shmodsi  31359  atcvati  32356  atcvat2i  32357  chirredlem4  32363  atmd2  32370  sumdmdlem  32388  addltmulALT  32416  iundisj2f  32560  iundisj2fi  32769  f1resveqaeq  35087  erdszelem9  35211  satffunlem1lem2  35415  satffunlem2lem2  35418  rdgprc  35807  cgrsub  36058  btwnxfr  36069  lineext  36089  linecgr  36094  btwnconn1lem4  36103  btwnconn1lem5  36104  btwnconn1lem6  36105  btwnconn1lem8  36107  btwnconn1lem11  36110  mptsnunlem  37351  finxpreclem6  37409  ltflcei  37627  poimirlem23  37662  poimirlem24  37663  poimirlem31  37670  poimirlem32  37671  ftc1anclem5  37716  heiborlem6  37835  grpokerinj  37912  dvrunz  37973  isdmn3  38093  dmncan1  38095  membpartlem19  38828  l1cvpat  39072  atnle  39335  cvlexch3  39350  cvlexch4N  39351  cvlatexchb1  39352  cvrat2  39447  atlelt  39456  3dimlem4a  39481  3dimlem4OLDN  39483  ps-1  39495  ps-2  39496  4atlem10  39624  4atlem11  39627  4atlem12  39630  cdleme11c  40279  cdleme21c  40345  cdlemg6d  40639  trlcoat  40741  tendoid0  40843  cdleml3N  40996  dia2dimlem7  41088  aks6d1c6lem3  42184  expeq1d  42336  fsuppind  42602  pellexlem1  42841  pellexlem6  42846  imasgim  43112  onsupmaxb  43251  safesnsupfidom1o  43429  reabsifnpos  43645  reabsifnneg  43647  iunrelexpmin1  43720  iunrelexpmin2  43724  radcnvrat  44326  nzss  44329  pwclaxpow  44996  ormkglobd  46892  elprneb  47039  or2expropbi  47044  tz6.12i-afv2  47253  dfatcolem  47265  f1oresf1o2  47301  zm1nn  47312  2ffzoeq  47337  modmkpkne  47371  sfprmdvdsmersenne  47613  lighneallem3  47617  lighneallem4  47620  requad01  47631  fppr2odd  47741  fpprwppr  47749  stgoldbwt  47786  sbgoldbaltlem1  47789  isuspgrimlem  47905  upgrimpthslem2  47918  isubgr3stgrlem4  47979  isubgr3stgrlem7  47982  gpg5nbgrvtx03starlem1  48078  gpg5nbgrvtx03starlem3  48080  gpg5nbgrvtx13starlem1  48081  gpg5nbgrvtx13starlem3  48083  lmod0rng  48239  lidldomn1  48241  rngcisoALTV  48287  ringcisoALTV  48321  ztprmneprm  48357  lincresunit3  48492  itsclc0yqsol  48775  itschlc0xyqsol1  48777  aacllem  49812