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  3621  eqreu  3703  sotr2  5583  sotr3  5590  sossfld  6162  ordintdif  6386  tz6.12i  6889  f1cofveqaeqALT  7236  soisoi  7306  riotaeqimp  7373  ov3  7555  tfindsg  7840  tfindsg2  7841  nnsuc  7863  findsg  7876  soseq  8141  suppssr  8177  suppssrg  8178  tfrlem9  8356  oe0lem  8480  oa00  8526  omwordi  8538  om00  8542  omass  8547  oelim2  8562  oeoa  8564  oeoe  8566  nnmwordi  8602  swoso  8708  dom2lem  8966  onsdominel  9096  f1finf1o  9223  f1finf1oOLD  9224  fiint  9284  cantnfp1lem3  9640  cantnfp1  9641  cantnflem1  9649  ttrclselem2  9686  rankr1ai  9758  rankval3b  9786  harcard  9938  infxpenlem  9973  alephnbtwn  10031  alephinit  10055  infxp  10174  cofsmo  10229  infpssALT  10273  fin23lem24  10282  fin56  10353  ttukeylem6  10474  ficard  10525  alephval2  10532  fpwwe2lem7  10597  fpwwe2  10603  gchdju1  10616  pwfseqlem3  10620  pwfseqlem4a  10621  pwfseqlem4  10622  gchpwdom  10630  tskss  10718  inar1  10735  gruss  10756  gruurn  10758  ltsonq  10929  distrlem4pr  10986  sqgt0sr  11066  map2psrpr  11070  letric  11281  renegcli  11490  addid0  11604  mulge0b  12060  nnge1  12221  0mnnnnn0  12481  nn0lt2  12604  zneo  12624  uzind2  12634  fzind  12639  nn0ind-raph  12641  uzwo  12877  nn01to3  12907  zbtwnre  12912  rpnnen1lem5  12947  ledivge1le  13031  xrletri  13120  qsqueeze  13168  difreicc  13452  elfzmlbp  13607  difelfznle  13610  elfzodifsumelfzo  13699  ssfzo12  13727  elfzonelfzo  13737  flflp1  13776  fleqceilz  13823  modsumfzodifsn  13916  addmodlteq  13918  om2uzf1oi  13925  expnngt1  14213  facdiv  14259  facwordi  14261  bcpasc  14293  hashdom  14351  hashgt23el  14396  hashdmpropge2  14455  ccatsymb  14554  swrdnnn0nd  14628  swrdnd0  14629  swrdsbslen  14636  swrdspsleq  14637  swrdlsw  14639  pfxnd0  14660  swrdswrdlem  14676  swrdccatin1  14697  pfxccatin12lem3  14704  swrdccat  14707  pfxccat3a  14710  repswswrd  14756  cshwidx0  14778  cshwcsh2id  14801  limsupbnd1  15455  lo1bdd2  15497  addcn2  15567  mulcn2  15569  o1rlimmul  15592  lo1add  15600  lo1mul  15601  rlimno1  15627  ruclem3  16208  odd2np1  16318  oddge22np1  16326  bitsfzo  16412  cncongr1  16644  2mulprm  16670  prm23ge5  16793  pcdvdsb  16847  pcaddlem  16866  infpnlem1  16888  prmunb  16892  vdwlem9  16967  vdwnnlem3  16975  ramcl  17007  prmgaplem5  17033  cshwshash  17082  setcmon  18056  setcepi  18057  setciso  18060  xpsmnd0  18712  f1ghm0to0  19184  ghmf1  19185  sylow2alem2  19555  sylow2blem3  19559  qusabl  19802  lt6abl  19832  cyggexb  19836  gsumcom2  19912  ringurd  20101  imasring  20246  xpsring1d  20249  0ring1eq0  20449  subrgdvds  20502  rngciso  20554  ringciso  20588  isdomn4  20632  drnginvrcl  20669  drnginvrl  20672  drnginvrr  20673  lsmelval2  20999  quscrng  21200  xrsdsreclblem  21336  obs2ss  21645  obslbs  21646  rnasclassa  21811  mplsubrglem  21920  psdmul  22060  gsummoncoe1  22202  mp2pm2mplem4  22703  chfacfisf  22748  chfacfisfcpmat  22749  cayleyhamilton1  22786  cmpsublem  23293  cmpsub  23294  1stccnp  23356  locfincf  23425  txhaus  23541  xkohaus  23547  ufilss  23799  cfinufil  23822  fmfnfmlem1  23848  hausflim  23875  fclscf  23919  alexsubb  23940  qustgplem  24015  prdsbl  24386  metss2lem  24406  nghmcn  24640  cfil3i  25176  cmetcaulem  25195  minveclem4  25339  ovolgelb  25388  ovolunnul  25408  ovoliun  25413  ovoliunnul  25415  ovolicc2lem2  25426  iundisj2  25457  voliunlem3  25460  rolle  25901  dvlip  25905  lhop1lem  25925  lhop2  25927  dvfsumrlim  25945  deg1ge  26010  coeeulem  26136  dgrco  26188  radcnvlt1  26334  psercnlem1  26342  logcnlem2  26559  logcnlem3  26560  cxpeq  26674  angpined  26747  efrlim  26886  efrlimOLD  26887  dmgmaddn0  26940  lgamucov  26955  basellem2  26999  ppieq0  27093  mumullem2  27097  chpeq0  27126  chteq0  27127  chtub  27130  fsumvma  27131  dchrptlem1  27182  bposlem6  27207  gausslemma2dlem0i  27282  gausslemma2dlem1a  27283  lgseisenlem2  27294  2sqlem6  27341  2sq2  27351  2sqnn0  27356  2sqreulem1  27364  2sqreunnlem1  27367  dchrisum0lem1  27434  pntrsumbnd2  27485  pntlem3  27527  noextenddif  27587  nosupno  27622  nosupbnd1  27633  noinfno  27637  noinfbnd1  27648  noetasuplem4  27655  noetainflem4  27659  scutun12  27729  slerec  27738  cutlt  27847  sleadd2im  27902  onsiso  28176  n0sfincut  28253  colinearalg  28844  eengtrkg  28920  incistruhgr  29013  wlkv0  29586  crctcshwlkn0  29758  clwwlkccatlem  29925  clwlkclwwlklem2a4  29933  clwlkclwwlklem2  29936  clwlkclwwlkfo  29945  eucrctshift  30179  frrusgrord0  30276  frgrreg  30330  blocni  30741  ubthlem1  30806  minvecolem4  30816  shmodsi  31325  atcvati  32322  atcvat2i  32323  chirredlem4  32329  atmd2  32336  sumdmdlem  32354  addltmulALT  32382  iundisj2f  32526  iundisj2fi  32727  f1resveqaeq  35082  erdszelem9  35193  satffunlem1lem2  35397  satffunlem2lem2  35400  rdgprc  35789  cgrsub  36040  btwnxfr  36051  lineext  36071  linecgr  36076  btwnconn1lem4  36085  btwnconn1lem5  36086  btwnconn1lem6  36087  btwnconn1lem8  36089  btwnconn1lem11  36092  mptsnunlem  37333  finxpreclem6  37391  ltflcei  37609  poimirlem23  37644  poimirlem24  37645  poimirlem31  37652  poimirlem32  37653  ftc1anclem5  37698  heiborlem6  37817  grpokerinj  37894  dvrunz  37955  isdmn3  38075  dmncan1  38077  membpartlem19  38810  l1cvpat  39054  atnle  39317  cvlexch3  39332  cvlexch4N  39333  cvlatexchb1  39334  cvrat2  39430  atlelt  39439  3dimlem4a  39464  3dimlem4OLDN  39466  ps-1  39478  ps-2  39479  4atlem10  39607  4atlem11  39610  4atlem12  39613  cdleme11c  40262  cdleme21c  40328  cdlemg6d  40622  trlcoat  40724  tendoid0  40826  cdleml3N  40979  dia2dimlem7  41071  aks6d1c6lem3  42167  expeq1d  42319  fsuppind  42585  pellexlem1  42824  pellexlem6  42829  imasgim  43096  onsupmaxb  43235  safesnsupfidom1o  43413  reabsifnpos  43629  reabsifnneg  43631  iunrelexpmin1  43704  iunrelexpmin2  43708  radcnvrat  44310  nzss  44313  pwclaxpow  44981  ormkglobd  46880  elprneb  47034  or2expropbi  47039  tz6.12i-afv2  47248  dfatcolem  47260  f1oresf1o2  47296  zm1nn  47307  2ffzoeq  47332  modmkpkne  47366  sfprmdvdsmersenne  47608  lighneallem3  47612  lighneallem4  47615  requad01  47626  fppr2odd  47736  fpprwppr  47744  stgoldbwt  47781  sbgoldbaltlem1  47784  isuspgrimlem  47899  upgrimpthslem2  47912  isubgr3stgrlem4  47972  isubgr3stgrlem7  47975  gpg5nbgrvtx03starlem1  48063  gpg5nbgrvtx03starlem3  48065  gpg5nbgrvtx13starlem1  48066  gpg5nbgrvtx13starlem3  48068  lmod0rng  48221  lidldomn1  48223  rngcisoALTV  48269  ringcisoALTV  48303  ztprmneprm  48339  lincresunit3  48474  itsclc0yqsol  48757  itschlc0xyqsol1  48759  aacllem  49794