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  3618  eqreu  3700  sotr2  5580  sotr3  5587  sossfld  6159  ordintdif  6383  tz6.12i  6886  f1cofveqaeqALT  7233  soisoi  7303  riotaeqimp  7370  ov3  7552  tfindsg  7837  tfindsg2  7838  nnsuc  7860  findsg  7873  soseq  8138  suppssr  8174  suppssrg  8175  tfrlem9  8353  oe0lem  8477  oa00  8523  omwordi  8535  om00  8539  omass  8544  oelim2  8559  oeoa  8561  oeoe  8563  nnmwordi  8599  swoso  8705  dom2lem  8963  onsdominel  9090  f1finf1o  9216  f1finf1oOLD  9217  fiint  9277  cantnfp1lem3  9633  cantnfp1  9634  cantnflem1  9642  ttrclselem2  9679  rankr1ai  9751  rankval3b  9779  harcard  9931  infxpenlem  9966  alephnbtwn  10024  alephinit  10048  infxp  10167  cofsmo  10222  infpssALT  10266  fin23lem24  10275  fin56  10346  ttukeylem6  10467  ficard  10518  alephval2  10525  fpwwe2lem7  10590  fpwwe2  10596  gchdju1  10609  pwfseqlem3  10613  pwfseqlem4a  10614  pwfseqlem4  10615  gchpwdom  10623  tskss  10711  inar1  10728  gruss  10749  gruurn  10751  ltsonq  10922  distrlem4pr  10979  sqgt0sr  11059  map2psrpr  11063  letric  11274  renegcli  11483  addid0  11597  mulge0b  12053  nnge1  12214  0mnnnnn0  12474  nn0lt2  12597  zneo  12617  uzind2  12627  fzind  12632  nn0ind-raph  12634  uzwo  12870  nn01to3  12900  zbtwnre  12905  rpnnen1lem5  12940  ledivge1le  13024  xrletri  13113  qsqueeze  13161  difreicc  13445  elfzmlbp  13600  difelfznle  13603  elfzodifsumelfzo  13692  ssfzo12  13720  elfzonelfzo  13730  flflp1  13769  fleqceilz  13816  modsumfzodifsn  13909  addmodlteq  13911  om2uzf1oi  13918  expnngt1  14206  facdiv  14252  facwordi  14254  bcpasc  14286  hashdom  14344  hashgt23el  14389  hashdmpropge2  14448  ccatsymb  14547  swrdnnn0nd  14621  swrdnd0  14622  swrdsbslen  14629  swrdspsleq  14630  swrdlsw  14632  pfxnd0  14653  swrdswrdlem  14669  swrdccatin1  14690  pfxccatin12lem3  14697  swrdccat  14700  pfxccat3a  14703  repswswrd  14749  cshwidx0  14771  cshwcsh2id  14794  limsupbnd1  15448  lo1bdd2  15490  addcn2  15560  mulcn2  15562  o1rlimmul  15585  lo1add  15593  lo1mul  15594  rlimno1  15620  ruclem3  16201  odd2np1  16311  oddge22np1  16319  bitsfzo  16405  cncongr1  16637  2mulprm  16663  prm23ge5  16786  pcdvdsb  16840  pcaddlem  16859  infpnlem1  16881  prmunb  16885  vdwlem9  16960  vdwnnlem3  16968  ramcl  17000  prmgaplem5  17026  cshwshash  17075  setcmon  18049  setcepi  18050  setciso  18053  xpsmnd0  18705  f1ghm0to0  19177  ghmf1  19178  sylow2alem2  19548  sylow2blem3  19552  qusabl  19795  lt6abl  19825  cyggexb  19829  gsumcom2  19905  ringurd  20094  imasring  20239  xpsring1d  20242  0ring1eq0  20442  subrgdvds  20495  rngciso  20547  ringciso  20581  isdomn4  20625  drnginvrcl  20662  drnginvrl  20665  drnginvrr  20666  lsmelval2  20992  quscrng  21193  xrsdsreclblem  21329  obs2ss  21638  obslbs  21639  rnasclassa  21804  mplsubrglem  21913  psdmul  22053  gsummoncoe1  22195  mp2pm2mplem4  22696  chfacfisf  22741  chfacfisfcpmat  22742  cayleyhamilton1  22779  cmpsublem  23286  cmpsub  23287  1stccnp  23349  locfincf  23418  txhaus  23534  xkohaus  23540  ufilss  23792  cfinufil  23815  fmfnfmlem1  23841  hausflim  23868  fclscf  23912  alexsubb  23933  qustgplem  24008  prdsbl  24379  metss2lem  24399  nghmcn  24633  cfil3i  25169  cmetcaulem  25188  minveclem4  25332  ovolgelb  25381  ovolunnul  25401  ovoliun  25406  ovoliunnul  25408  ovolicc2lem2  25419  iundisj2  25450  voliunlem3  25453  rolle  25894  dvlip  25898  lhop1lem  25918  lhop2  25920  dvfsumrlim  25938  deg1ge  26003  coeeulem  26129  dgrco  26181  radcnvlt1  26327  psercnlem1  26335  logcnlem2  26552  logcnlem3  26553  cxpeq  26667  angpined  26740  efrlim  26879  efrlimOLD  26880  dmgmaddn0  26933  lgamucov  26948  basellem2  26992  ppieq0  27086  mumullem2  27090  chpeq0  27119  chteq0  27120  chtub  27123  fsumvma  27124  dchrptlem1  27175  bposlem6  27200  gausslemma2dlem0i  27275  gausslemma2dlem1a  27276  lgseisenlem2  27287  2sqlem6  27334  2sq2  27344  2sqnn0  27349  2sqreulem1  27357  2sqreunnlem1  27360  dchrisum0lem1  27427  pntrsumbnd2  27478  pntlem3  27520  noextenddif  27580  nosupno  27615  nosupbnd1  27626  noinfno  27630  noinfbnd1  27641  noetasuplem4  27648  noetainflem4  27652  scutun12  27722  slerec  27731  cutlt  27840  sleadd2im  27895  onsiso  28169  n0sfincut  28246  colinearalg  28837  eengtrkg  28913  incistruhgr  29006  wlkv0  29579  crctcshwlkn0  29751  clwwlkccatlem  29918  clwlkclwwlklem2a4  29926  clwlkclwwlklem2  29929  clwlkclwwlkfo  29938  eucrctshift  30172  frrusgrord0  30269  frgrreg  30323  blocni  30734  ubthlem1  30799  minvecolem4  30809  shmodsi  31318  atcvati  32315  atcvat2i  32316  chirredlem4  32322  atmd2  32329  sumdmdlem  32347  addltmulALT  32375  iundisj2f  32519  iundisj2fi  32720  f1resveqaeq  35075  erdszelem9  35186  satffunlem1lem2  35390  satffunlem2lem2  35393  rdgprc  35782  cgrsub  36033  btwnxfr  36044  lineext  36064  linecgr  36069  btwnconn1lem4  36078  btwnconn1lem5  36079  btwnconn1lem6  36080  btwnconn1lem8  36082  btwnconn1lem11  36085  mptsnunlem  37326  finxpreclem6  37384  ltflcei  37602  poimirlem23  37637  poimirlem24  37638  poimirlem31  37645  poimirlem32  37646  ftc1anclem5  37691  heiborlem6  37810  grpokerinj  37887  dvrunz  37948  isdmn3  38068  dmncan1  38070  membpartlem19  38803  l1cvpat  39047  atnle  39310  cvlexch3  39325  cvlexch4N  39326  cvlatexchb1  39327  cvrat2  39423  atlelt  39432  3dimlem4a  39457  3dimlem4OLDN  39459  ps-1  39471  ps-2  39472  4atlem10  39600  4atlem11  39603  4atlem12  39606  cdleme11c  40255  cdleme21c  40321  cdlemg6d  40615  trlcoat  40717  tendoid0  40819  cdleml3N  40972  dia2dimlem7  41064  aks6d1c6lem3  42160  expeq1d  42312  fsuppind  42578  pellexlem1  42817  pellexlem6  42822  imasgim  43089  onsupmaxb  43228  safesnsupfidom1o  43406  reabsifnpos  43622  reabsifnneg  43624  iunrelexpmin1  43697  iunrelexpmin2  43701  radcnvrat  44303  nzss  44306  pwclaxpow  44974  ormkglobd  46873  elprneb  47030  or2expropbi  47035  tz6.12i-afv2  47244  dfatcolem  47256  f1oresf1o2  47292  zm1nn  47303  2ffzoeq  47328  modmkpkne  47362  sfprmdvdsmersenne  47604  lighneallem3  47608  lighneallem4  47611  requad01  47622  fppr2odd  47732  fpprwppr  47740  stgoldbwt  47777  sbgoldbaltlem1  47780  isuspgrimlem  47895  upgrimpthslem2  47908  isubgr3stgrlem4  47968  isubgr3stgrlem7  47971  gpg5nbgrvtx03starlem1  48059  gpg5nbgrvtx03starlem3  48061  gpg5nbgrvtx13starlem1  48062  gpg5nbgrvtx13starlem3  48064  lmod0rng  48217  lidldomn1  48219  rngcisoALTV  48265  ringcisoALTV  48299  ztprmneprm  48335  lincresunit3  48470  itsclc0yqsol  48753  itschlc0xyqsol1  48755  aacllem  49790