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 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  293  ceqex  3641  eqreu  3726  sotr2  5621  sotr3  5628  sossfld  6186  ordintdif  6415  tz6.12i  6920  f1cofveqaeqALT  7258  soisoi  7325  riotaeqimp  7392  ov3  7570  tfindsg  7850  tfindsg2  7851  nnsuc  7873  findsg  7890  soseq  8145  suppssr  8181  suppssrg  8182  tfrlem9  8385  oe0lem  8513  oa00  8559  omwordi  8571  om00  8575  omass  8580  oelim2  8595  oeoa  8597  oeoe  8599  nnmwordi  8635  swoso  8736  dom2lem  8988  onsdominel  9126  f1finf1o  9271  f1finf1oOLD  9272  cantnfp1lem3  9675  cantnfp1  9676  cantnflem1  9684  ttrclselem2  9721  rankr1ai  9793  rankval3b  9821  harcard  9973  infxpenlem  10008  alephnbtwn  10066  alephinit  10090  infxp  10210  cofsmo  10264  infpssALT  10308  fin23lem24  10317  fin56  10388  ttukeylem6  10509  ficard  10560  alephval2  10567  fpwwe2lem7  10632  fpwwe2  10638  gchdju1  10651  pwfseqlem3  10655  pwfseqlem4a  10656  pwfseqlem4  10657  gchpwdom  10665  tskss  10753  inar1  10770  gruss  10791  gruurn  10793  ltsonq  10964  distrlem4pr  11021  sqgt0sr  11101  map2psrpr  11105  letric  11314  renegcli  11521  addid0  11633  mulge0b  12084  nnge1  12240  0mnnnnn0  12504  nn0lt2  12625  zneo  12645  uzind2  12655  fzind  12660  nn0ind-raph  12662  uzwo  12895  nn01to3  12925  zbtwnre  12930  rpnnen1lem5  12965  ledivge1le  13045  xrletri  13132  qsqueeze  13180  difreicc  13461  elfzmlbp  13612  difelfznle  13615  elfzodifsumelfzo  13698  ssfzo12  13725  elfzonelfzo  13734  flflp1  13772  fleqceilz  13819  modsumfzodifsn  13909  addmodlteq  13911  om2uzf1oi  13918  expnngt1  14204  facdiv  14247  facwordi  14249  bcpasc  14281  hashdom  14339  hashgt23el  14384  hashdmpropge2  14444  ccatsymb  14532  swrdnnn0nd  14606  swrdnd0  14607  swrdsbslen  14614  swrdspsleq  14615  swrdlsw  14617  pfxnd0  14638  swrdswrdlem  14654  swrdccatin1  14675  pfxccatin12lem3  14682  swrdccat  14685  pfxccat3a  14688  repswswrd  14734  cshwidx0  14756  cshwcsh2id  14779  limsupbnd1  15426  lo1bdd2  15468  addcn2  15538  mulcn2  15540  o1rlimmul  15563  lo1add  15571  lo1mul  15572  rlimno1  15600  ruclem3  16176  odd2np1  16284  oddge22np1  16292  bitsfzo  16376  cncongr1  16604  2mulprm  16630  prm23ge5  16748  pcdvdsb  16802  pcaddlem  16821  infpnlem1  16843  prmunb  16847  vdwlem9  16922  vdwnnlem3  16930  ramcl  16962  prmgaplem5  16988  cshwshash  17038  setcmon  18037  setcepi  18038  setciso  18041  xpsmnd0  18666  ghmf1  19121  sylow2alem2  19486  sylow2blem3  19490  qusabl  19733  lt6abl  19763  cyggexb  19767  gsumcom2  19843  ringurd  20008  imasring  20143  xpsring1d  20146  f1ghm0to0  20279  subrgdvds  20333  drnginvrcl  20379  drnginvrl  20382  drnginvrr  20383  lsmelval2  20696  quscrng  20878  isdomn4  20918  xrsdsreclblem  20991  obs2ss  21284  obslbs  21285  rnasclassa  21449  mplsubrglem  21563  gsummoncoe1  21828  mp2pm2mplem4  22311  chfacfisf  22356  chfacfisfcpmat  22357  cayleyhamilton1  22394  cmpsublem  22903  cmpsub  22904  1stccnp  22966  locfincf  23035  txhaus  23151  xkohaus  23157  ufilss  23409  cfinufil  23432  fmfnfmlem1  23458  hausflim  23485  fclscf  23529  alexsubb  23550  qustgplem  23625  prdsbl  24000  metss2lem  24020  nghmcn  24262  cfil3i  24786  cmetcaulem  24805  minveclem4  24949  ovolgelb  24997  ovolunnul  25017  ovoliun  25022  ovoliunnul  25024  ovolicc2lem2  25035  iundisj2  25066  voliunlem3  25069  rolle  25507  dvlip  25510  lhop1lem  25530  lhop2  25532  dvfsumrlim  25548  deg1ge  25616  coeeulem  25738  dgrco  25789  radcnvlt1  25930  psercnlem1  25937  logcnlem2  26151  logcnlem3  26152  cxpeq  26265  angpined  26335  efrlim  26474  dmgmaddn0  26527  lgamucov  26542  basellem2  26586  ppieq0  26680  mumullem2  26684  chpeq0  26711  chteq0  26712  chtub  26715  fsumvma  26716  dchrptlem1  26767  bposlem6  26792  gausslemma2dlem0i  26867  gausslemma2dlem1a  26868  lgseisenlem2  26879  2sqlem6  26926  2sq2  26936  2sqnn0  26941  2sqreulem1  26949  2sqreunnlem1  26952  dchrisum0lem1  27019  pntrsumbnd2  27070  pntlem3  27112  noextenddif  27171  nosupno  27206  nosupbnd1  27217  noinfno  27221  noinfbnd1  27232  noetasuplem4  27239  noetainflem4  27243  scutun12  27311  slerec  27320  cutlt  27419  sleadd2im  27471  colinearalg  28168  eengtrkg  28244  incistruhgr  28339  wlkv0  28908  crctcshwlkn0  29075  clwwlkccatlem  29242  clwlkclwwlklem2a4  29250  clwlkclwwlklem2  29253  clwlkclwwlkfo  29262  eucrctshift  29496  frrusgrord0  29593  frgrreg  29647  blocni  30058  ubthlem1  30123  minvecolem4  30133  shmodsi  30642  atcvati  31639  atcvat2i  31640  chirredlem4  31646  atmd2  31653  sumdmdlem  31671  addltmulALT  31699  iundisj2f  31821  iundisj2fi  32008  f1resveqaeq  34088  erdszelem9  34190  satffunlem1lem2  34394  satffunlem2lem2  34397  rdgprc  34766  cgrsub  35017  btwnxfr  35028  lineext  35048  linecgr  35053  btwnconn1lem4  35062  btwnconn1lem5  35063  btwnconn1lem6  35064  btwnconn1lem8  35066  btwnconn1lem11  35069  mptsnunlem  36219  finxpreclem6  36277  ltflcei  36476  poimirlem23  36511  poimirlem24  36512  poimirlem31  36519  poimirlem32  36520  ftc1anclem5  36565  heiborlem6  36684  grpokerinj  36761  dvrunz  36822  isdmn3  36942  dmncan1  36944  membpartlem19  37681  l1cvpat  37924  atnle  38187  cvlexch3  38202  cvlexch4N  38203  cvlatexchb1  38204  cvrat2  38300  atlelt  38309  3dimlem4a  38334  3dimlem4OLDN  38336  ps-1  38348  ps-2  38349  4atlem10  38477  4atlem11  38480  4atlem12  38483  cdleme11c  39132  cdleme21c  39198  cdlemg6d  39492  trlcoat  39594  tendoid0  39696  cdleml3N  39849  dia2dimlem7  39941  metakunt1  40985  metakunt6  40990  fsuppind  41162  pellexlem1  41567  pellexlem6  41572  imasgim  41842  onsupmaxb  41988  safesnsupfidom1o  42168  reabsifnpos  42384  reabsifnneg  42386  iunrelexpmin1  42459  iunrelexpmin2  42463  radcnvrat  43073  nzss  43076  elprneb  45739  or2expropbi  45744  tz6.12i-afv2  45951  dfatcolem  45963  f1oresf1o2  45999  zm1nn  46010  2ffzoeq  46036  sfprmdvdsmersenne  46271  lighneallem3  46275  lighneallem4  46278  requad01  46289  fppr2odd  46399  fpprwppr  46407  stgoldbwt  46444  sbgoldbaltlem1  46447  isomuspgrlem1  46495  lmod0rng  46642  0ring1eq0  46646  lidldomn1  46823  rngciso  46880  rngcisoALTV  46892  ringciso  46931  ringcisoALTV  46955  ztprmneprm  47023  lincresunit3  47162  itsclc0yqsol  47450  itschlc0xyqsol1  47452  aacllem  47848