Theorem sylbird 259

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 247	. 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  292  ceqex  3582  eqreu  3667  sotr2  5534  sossfld  6086  ordintdif  6312  tz6.12i  6794  f1cofveqaeqALT  7126  soisoi  7192  riotaeqimp  7252  ov3  7426  tfindsg  7695  tfindsg2  7696  nnsuc  7718  findsg  7733  suppssr  7996  suppssrg  7997  tfrlem9  8200  oe0lem  8319  oa00  8366  omwordi  8378  om00  8382  omass  8387  oelim2  8402  oeoa  8404  oeoe  8406  nnmwordi  8442  swoso  8505  dom2lem  8751  onsdominel  8878  f1finf1o  9007  cantnfp1lem3  9399  cantnfp1  9400  cantnflem1  9408  ttrclselem2  9445  rankr1ai  9540  rankval3b  9568  harcard  9720  infxpenlem  9753  alephnbtwn  9811  alephinit  9835  infxp  9955  cofsmo  10009  infpssALT  10053  fin23lem24  10062  fin56  10133  ttukeylem6  10254  ficard  10305  alephval2  10312  fpwwe2lem7  10377  fpwwe2  10383  gchdju1  10396  pwfseqlem3  10400  pwfseqlem4a  10401  pwfseqlem4  10402  gchpwdom  10410  tskss  10498  inar1  10515  gruss  10536  gruurn  10538  ltsonq  10709  distrlem4pr  10766  sqgt0sr  10846  map2psrpr  10850  letric  11058  renegcli  11265  addid0  11377  mulge0b  11828  nnge1  11984  0mnnnnn0  12248  nn0lt2  12366  zneo  12386  uzind2  12396  fzind  12401  nn0ind-raph  12403  uzwo  12633  nn01to3  12663  zbtwnre  12668  rpnnen1lem5  12703  ledivge1le  12783  xrletri  12869  qsqueeze  12917  difreicc  13198  elfzmlbp  13349  difelfznle  13352  elfzodifsumelfzo  13434  ssfzo12  13461  elfzonelfzo  13470  flflp1  13508  fleqceilz  13555  modsumfzodifsn  13645  addmodlteq  13647  om2uzf1oi  13654  expnngt1  13937  facdiv  13982  facwordi  13984  bcpasc  14016  hashdom  14075  hashgt23el  14120  hashdmpropge2  14178  ccatsymb  14268  swrdnnn0nd  14350  swrdnd0  14351  swrdsbslen  14358  swrdspsleq  14359  swrdlsw  14361  pfxnd0  14382  swrdswrdlem  14398  swrdccatin1  14419  pfxccatin12lem3  14426  swrdccat  14429  pfxccat3a  14432  repswswrd  14478  cshwidx0  14500  cshwcsh2id  14522  limsupbnd1  15172  lo1bdd2  15214  addcn2  15284  mulcn2  15286  o1rlimmul  15309  lo1add  15317  lo1mul  15318  rlimno1  15346  ruclem3  15923  odd2np1  16031  oddge22np1  16039  bitsfzo  16123  cncongr1  16353  2mulprm  16379  prm23ge5  16497  pcdvdsb  16551  pcaddlem  16570  infpnlem1  16592  prmunb  16596  vdwlem9  16671  vdwnnlem3  16679  ramcl  16711  prmgaplem5  16737  cshwshash  16787  setcmon  17783  setcepi  17784  setciso  17787  ghmf1  18844  sylow2alem2  19204  sylow2blem3  19208  qusabl  19447  lt6abl  19477  cyggexb  19481  gsumcom2  19557  imasring  19839  f1ghm0to0  19965  drnginvrcl  19989  drnginvrl  19991  drnginvrr  19992  subrgdvds  20019  lsmelval2  20328  quscrng  20492  xrsdsreclblem  20625  obs2ss  20917  obslbs  20918  rnasclassa  21080  mplsubrglem  21191  gsummoncoe1  21456  mp2pm2mplem4  21939  chfacfisf  21984  chfacfisfcpmat  21985  cayleyhamilton1  22022  cmpsublem  22531  cmpsub  22532  1stccnp  22594  locfincf  22663  txhaus  22779  xkohaus  22785  ufilss  23037  cfinufil  23060  fmfnfmlem1  23086  hausflim  23113  fclscf  23157  alexsubb  23178  qustgplem  23253  prdsbl  23628  metss2lem  23648  nghmcn  23890  cfil3i  24414  cmetcaulem  24433  minveclem4  24577  ovolgelb  24625  ovolunnul  24645  ovoliun  24650  ovoliunnul  24652  ovolicc2lem2  24663  iundisj2  24694  voliunlem3  24697  rolle  25135  dvlip  25138  lhop1lem  25158  lhop2  25160  dvfsumrlim  25176  deg1ge  25244  coeeulem  25366  dgrco  25417  radcnvlt1  25558  psercnlem1  25565  logcnlem2  25779  logcnlem3  25780  cxpeq  25891  angpined  25961  efrlim  26100  dmgmaddn0  26153  lgamucov  26168  basellem2  26212  ppieq0  26306  mumullem2  26310  chpeq0  26337  chteq0  26338  chtub  26341  fsumvma  26342  dchrptlem1  26393  bposlem6  26418  gausslemma2dlem0i  26493  gausslemma2dlem1a  26494  lgseisenlem2  26505  2sqlem6  26552  2sq2  26562  2sqnn0  26567  2sqreulem1  26575  2sqreunnlem1  26578  dchrisum0lem1  26645  pntrsumbnd2  26696  pntlem3  26738  colinearalg  27259  eengtrkg  27335  incistruhgr  27430  wlkv0  27998  crctcshwlkn0  28165  clwwlkccatlem  28332  clwlkclwwlklem2a4  28340  clwlkclwwlklem2  28343  clwlkclwwlkfo  28352  eucrctshift  28586  frrusgrord0  28683  frgrreg  28737  blocni  29146  ubthlem1  29211  minvecolem4  29221  shmodsi  29730  atcvati  30727  atcvat2i  30728  chirredlem4  30734  atmd2  30741  sumdmdlem  30759  addltmulALT  30787  iundisj2f  30908  iundisj2fi  31097  rngurd  31461  f1resveqaeq  33036  erdszelem9  33140  satffunlem1lem2  33344  satffunlem2lem2  33347  sotr3  33712  rdgprc  33749  soseq  33782  noextenddif  33850  nosupno  33885  nosupbnd1  33896  noinfno  33900  noinfbnd1  33911  noetasuplem4  33918  noetainflem4  33922  scutun12  33983  slerec  33992  cgrsub  34326  btwnxfr  34337  lineext  34357  linecgr  34362  btwnconn1lem4  34371  btwnconn1lem5  34372  btwnconn1lem6  34373  btwnconn1lem8  34375  btwnconn1lem11  34378  mptsnunlem  35488  finxpreclem6  35546  ltflcei  35744  poimirlem23  35779  poimirlem24  35780  poimirlem31  35787  poimirlem32  35788  ftc1anclem5  35833  heiborlem6  35953  grpokerinj  36030  dvrunz  36091  isdmn3  36211  dmncan1  36213  l1cvpat  37047  atnle  37310  cvlexch3  37325  cvlexch4N  37326  cvlatexchb1  37327  cvrat2  37422  atlelt  37431  3dimlem4a  37456  3dimlem4OLDN  37458  ps-1  37470  ps-2  37471  4atlem10  37599  4atlem11  37602  4atlem12  37605  cdleme11c  38254  cdleme21c  38320  cdlemg6d  38614  trlcoat  38716  tendoid0  38818  cdleml3N  38971  dia2dimlem7  39063  metakunt1  40105  metakunt6  40110  isdomn4  40152  fsuppind  40259  pellexlem1  40631  pellexlem6  40636  imasgim  40905  reabsifnpos  41194  reabsifnneg  41196  iunrelexpmin1  41269  iunrelexpmin2  41273  radcnvrat  41885  nzss  41888  elprneb  44474  or2expropbi  44479  tz6.12i-afv2  44686  dfatcolem  44698  f1oresf1o2  44734  zm1nn  44746  2ffzoeq  44772  sfprmdvdsmersenne  45007  lighneallem3  45011  lighneallem4  45014  requad01  45025  fppr2odd  45135  fpprwppr  45143  stgoldbwt  45180  sbgoldbaltlem1  45183  isomuspgrlem1  45231  lmod0rng  45378  0ring1eq0  45382  lidldomn1  45431  rngciso  45492  rngcisoALTV  45504  ringciso  45543  ringcisoALTV  45567  ztprmneprm  45635  lincresunit3  45774  itsclc0yqsol  46062  itschlc0xyqsol1  46064  aacllem  46457