Theorem sylbird 262

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 250	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
3		sylbird.2	. 2 ⊢ (𝜑 → (𝜒 → 𝜃))
4	2, 3	syld 47	1 ⊢ (𝜑 → (𝜓 → 𝜃))

Syntax hints:   → wi 4   ↔ wb 208

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 209

This theorem is referenced by:  3imtr3d  295  ceqex  3644  eqreu  3719  sotr2  5504  sossfld  6042  ordintdif  6239  tz6.12i  6695  f1cofveqaeqALT  7016  soisoi  7080  riotaeqimp  7139  ov3  7310  tfindsg  7574  tfindsg2  7575  nnsuc  7596  findsg  7608  suppssr  7860  tfrlem9  8020  oe0lem  8137  oa00  8184  omwordi  8196  om00  8200  omass  8205  oelim2  8220  oeoa  8222  oeoe  8224  nnmwordi  8260  swoso  8321  dom2lem  8548  onsdominel  8665  f1finf1o  8744  cantnfp1lem3  9142  cantnfp1  9143  cantnflem1  9151  rankr1ai  9226  rankval3b  9254  harcard  9406  infxpenlem  9438  alephnbtwn  9496  alephinit  9520  infxp  9636  cofsmo  9690  infpssALT  9734  fin23lem24  9743  fin56  9814  ttukeylem6  9935  ficard  9986  alephval2  9993  fpwwe2lem8  10058  fpwwe2  10064  gchdju1  10077  pwfseqlem3  10081  pwfseqlem4a  10082  pwfseqlem4  10083  gchpwdom  10091  tskss  10179  inar1  10196  gruss  10217  gruurn  10219  ltsonq  10390  distrlem4pr  10447  sqgt0sr  10527  map2psrpr  10531  letric  10739  renegcli  10946  addid0  11058  mulge0b  11509  nnge1  11664  0mnnnnn0  11928  nn0lt2  12044  zneo  12064  uzind2  12074  fzind  12079  nn0ind-raph  12081  uzwo  12310  nn01to3  12340  zbtwnre  12345  rpnnen1lem5  12379  ledivge1le  12459  xrletri  12545  qsqueeze  12593  difreicc  12869  elfzmlbp  13017  difelfznle  13020  elfzodifsumelfzo  13102  ssfzo12  13129  elfzonelfzo  13138  flflp1  13176  fleqceilz  13221  modsumfzodifsn  13311  addmodlteq  13313  om2uzf1oi  13320  expnngt1  13601  facdiv  13646  facwordi  13648  bcpasc  13680  hashdom  13739  hashgt23el  13784  hashdmpropge2  13840  ccatsymb  13935  swrdnnn0nd  14017  swrdnd0  14018  swrdsbslen  14025  swrdspsleq  14026  swrdlsw  14028  pfxnd0  14049  swrdswrdlem  14065  swrdccatin1  14086  pfxccatin12lem3  14093  swrdccat  14096  pfxccat3a  14099  repswswrd  14145  cshwidx0  14167  cshwcsh2id  14189  limsupbnd1  14838  lo1bdd2  14880  addcn2  14949  mulcn2  14951  o1rlimmul  14974  lo1add  14982  lo1mul  14983  rlimno1  15009  ruclem3  15585  odd2np1  15689  oddge22np1  15697  bitsfzo  15783  cncongr1  16010  2mulprm  16036  prm23ge5  16151  pcdvdsb  16204  pcaddlem  16223  infpnlem1  16245  prmunb  16249  vdwlem9  16324  vdwnnlem3  16332  ramcl  16364  prmgaplem5  16390  cshwshash  16437  setcmon  17346  setcepi  17347  setciso  17350  ghmf1  18386  sylow2alem2  18742  sylow2blem3  18746  qusabl  18984  lt6abl  19014  cyggexb  19018  gsumcom2  19094  imasring  19368  f1ghm0to0  19491  f1rhm0to0OLD  19492  drnginvrcl  19518  drnginvrl  19520  drnginvrr  19521  subrgdvds  19548  lsmelval2  19856  quscrng  20012  rnasclassa  20123  mplsubrglem  20218  gsummoncoe1  20471  xrsdsreclblem  20590  obs2ss  20872  obslbs  20873  mp2pm2mplem4  21416  chfacfisf  21461  chfacfisfcpmat  21462  cayleyhamilton1  21499  cmpsublem  22006  cmpsub  22007  1stccnp  22069  locfincf  22138  txhaus  22254  xkohaus  22260  ufilss  22512  cfinufil  22535  fmfnfmlem1  22561  hausflim  22588  fclscf  22632  alexsubb  22653  qustgplem  22728  prdsbl  23100  metss2lem  23120  nghmcn  23353  cfil3i  23871  cmetcaulem  23890  minveclem4  24034  ovolgelb  24080  ovolunnul  24100  ovoliun  24105  ovoliunnul  24107  ovolicc2lem2  24118  iundisj2  24149  voliunlem3  24152  rolle  24586  dvlip  24589  lhop1lem  24609  lhop2  24611  dvfsumrlim  24627  deg1ge  24691  coeeulem  24813  dgrco  24864  radcnvlt1  25005  psercnlem1  25012  logcnlem2  25225  logcnlem3  25226  cxpeq  25337  angpined  25407  efrlim  25546  dmgmaddn0  25599  lgamucov  25614  basellem2  25658  ppieq0  25752  mumullem2  25756  chpeq0  25783  chteq0  25784  chtub  25787  fsumvma  25788  dchrptlem1  25839  bposlem6  25864  gausslemma2dlem0i  25939  gausslemma2dlem1a  25940  lgseisenlem2  25951  2sqlem6  25998  2sq2  26008  2sqnn0  26013  2sqreulem1  26021  2sqreunnlem1  26024  dchrisum0lem1  26091  pntrsumbnd2  26142  pntlem3  26184  colinearalg  26695  eengtrkg  26771  incistruhgr  26863  wlkv0  27431  crctcshwlkn0  27598  clwwlkccatlem  27766  clwlkclwwlklem2a4  27774  clwlkclwwlklem2  27777  clwlkclwwlkfo  27786  eucrctshift  28021  frrusgrord0  28118  frgrreg  28172  blocni  28581  ubthlem1  28646  minvecolem4  28656  shmodsi  29165  atcvati  30162  atcvat2i  30163  chirredlem4  30169  atmd2  30176  sumdmdlem  30194  addltmulALT  30222  iundisj2f  30339  iundisj2fi  30519  rngurd  30857  f1resveqaeq  32358  erdszelem9  32446  satffunlem1lem2  32650  satffunlem2lem2  32653  sotr3  33002  rdgprc  33039  soseq  33096  noextenddif  33175  nosupno  33203  nosupbnd1  33214  noetalem3  33219  scutun12  33271  slerec  33277  cgrsub  33506  btwnxfr  33517  lineext  33537  linecgr  33542  btwnconn1lem4  33551  btwnconn1lem5  33552  btwnconn1lem6  33553  btwnconn1lem8  33555  btwnconn1lem11  33558  mptsnunlem  34618  finxpreclem6  34676  ltflcei  34879  poimirlem23  34914  poimirlem24  34915  poimirlem31  34922  poimirlem32  34923  ftc1anclem5  34970  heiborlem6  35093  grpokerinj  35170  dvrunz  35231  isdmn3  35351  dmncan1  35353  l1cvpat  36189  atnle  36452  cvlexch3  36467  cvlexch4N  36468  cvlatexchb1  36469  cvrat2  36564  atlelt  36573  3dimlem4a  36598  3dimlem4OLDN  36600  ps-1  36612  ps-2  36613  4atlem10  36741  4atlem11  36744  4atlem12  36747  cdleme11c  37396  cdleme21c  37462  cdlemg6d  37756  trlcoat  37858  tendoid0  37960  cdleml3N  38113  dia2dimlem7  38205  pellexlem1  39424  pellexlem6  39429  imasgim  39698  iunrelexpmin1  40051  iunrelexpmin2  40055  radcnvrat  40644  nzss  40647  elprneb  43263  or2expropbi  43268  tz6.12i-afv2  43441  dfatcolem  43453  f1oresf1o2  43489  zm1nn  43501  2ffzoeq  43527  sfprmdvdsmersenne  43767  lighneallem3  43771  lighneallem4  43774  requad01  43785  fppr2odd  43895  fpprwppr  43903  stgoldbwt  43940  sbgoldbaltlem1  43943  isomuspgrlem1  43991  lmod0rng  44138  0ring1eq0  44142  lidldomn1  44191  rngciso  44252  rngcisoALTV  44264  ringciso  44303  ringcisoALTV  44327  ztprmneprm  44394  lincresunit3  44535  itsclc0yqsol  44750  itschlc0xyqsol1  44752  aacllem  44901