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  3631  eqreu  3712  sotr2  5595  sotr3  5602  sossfld  6175  ordintdif  6403  tz6.12i  6903  f1cofveqaeqALT  7250  soisoi  7320  riotaeqimp  7386  ov3  7568  tfindsg  7854  tfindsg2  7855  nnsuc  7877  findsg  7891  soseq  8156  suppssr  8192  suppssrg  8193  tfrlem9  8397  oe0lem  8523  oa00  8569  omwordi  8581  om00  8585  omass  8590  oelim2  8605  oeoa  8607  oeoe  8609  nnmwordi  8645  swoso  8751  dom2lem  9004  onsdominel  9138  f1finf1o  9275  f1finf1oOLD  9276  fiint  9336  cantnfp1lem3  9692  cantnfp1  9693  cantnflem1  9701  ttrclselem2  9738  rankr1ai  9810  rankval3b  9838  harcard  9990  infxpenlem  10025  alephnbtwn  10083  alephinit  10107  infxp  10226  cofsmo  10281  infpssALT  10325  fin23lem24  10334  fin56  10405  ttukeylem6  10526  ficard  10577  alephval2  10584  fpwwe2lem7  10649  fpwwe2  10655  gchdju1  10668  pwfseqlem3  10672  pwfseqlem4a  10673  pwfseqlem4  10674  gchpwdom  10682  tskss  10770  inar1  10787  gruss  10808  gruurn  10810  ltsonq  10981  distrlem4pr  11038  sqgt0sr  11118  map2psrpr  11122  letric  11333  renegcli  11542  addid0  11654  mulge0b  12110  nnge1  12266  0mnnnnn0  12531  nn0lt2  12654  zneo  12674  uzind2  12684  fzind  12689  nn0ind-raph  12691  uzwo  12925  nn01to3  12955  zbtwnre  12960  rpnnen1lem5  12995  ledivge1le  13078  xrletri  13167  qsqueeze  13215  difreicc  13499  elfzmlbp  13654  difelfznle  13657  elfzodifsumelfzo  13745  ssfzo12  13773  elfzonelfzo  13783  flflp1  13822  fleqceilz  13869  modsumfzodifsn  13960  addmodlteq  13962  om2uzf1oi  13969  expnngt1  14257  facdiv  14303  facwordi  14305  bcpasc  14337  hashdom  14395  hashgt23el  14440  hashdmpropge2  14499  ccatsymb  14598  swrdnnn0nd  14672  swrdnd0  14673  swrdsbslen  14680  swrdspsleq  14681  swrdlsw  14683  pfxnd0  14704  swrdswrdlem  14720  swrdccatin1  14741  pfxccatin12lem3  14748  swrdccat  14751  pfxccat3a  14754  repswswrd  14800  cshwidx0  14822  cshwcsh2id  14845  limsupbnd1  15496  lo1bdd2  15538  addcn2  15608  mulcn2  15610  o1rlimmul  15633  lo1add  15641  lo1mul  15642  rlimno1  15668  ruclem3  16249  odd2np1  16358  oddge22np1  16366  bitsfzo  16452  cncongr1  16684  2mulprm  16710  prm23ge5  16833  pcdvdsb  16887  pcaddlem  16906  infpnlem1  16928  prmunb  16932  vdwlem9  17007  vdwnnlem3  17015  ramcl  17047  prmgaplem5  17073  cshwshash  17122  setcmon  18098  setcepi  18099  setciso  18102  xpsmnd0  18754  f1ghm0to0  19226  ghmf1  19227  sylow2alem2  19597  sylow2blem3  19601  qusabl  19844  lt6abl  19874  cyggexb  19878  gsumcom2  19954  ringurd  20143  imasring  20288  xpsring1d  20291  0ring1eq0  20491  subrgdvds  20544  rngciso  20596  ringciso  20630  isdomn4  20674  drnginvrcl  20711  drnginvrl  20714  drnginvrr  20715  lsmelval2  21041  quscrng  21242  xrsdsreclblem  21378  obs2ss  21687  obslbs  21688  rnasclassa  21853  mplsubrglem  21962  psdmul  22102  gsummoncoe1  22244  mp2pm2mplem4  22745  chfacfisf  22790  chfacfisfcpmat  22791  cayleyhamilton1  22828  cmpsublem  23335  cmpsub  23336  1stccnp  23398  locfincf  23467  txhaus  23583  xkohaus  23589  ufilss  23841  cfinufil  23864  fmfnfmlem1  23890  hausflim  23917  fclscf  23961  alexsubb  23982  qustgplem  24057  prdsbl  24428  metss2lem  24448  nghmcn  24682  cfil3i  25219  cmetcaulem  25238  minveclem4  25382  ovolgelb  25431  ovolunnul  25451  ovoliun  25456  ovoliunnul  25458  ovolicc2lem2  25469  iundisj2  25500  voliunlem3  25503  rolle  25944  dvlip  25948  lhop1lem  25968  lhop2  25970  dvfsumrlim  25988  deg1ge  26053  coeeulem  26179  dgrco  26231  radcnvlt1  26377  psercnlem1  26385  logcnlem2  26602  logcnlem3  26603  cxpeq  26717  angpined  26790  efrlim  26929  efrlimOLD  26930  dmgmaddn0  26983  lgamucov  26998  basellem2  27042  ppieq0  27136  mumullem2  27140  chpeq0  27169  chteq0  27170  chtub  27173  fsumvma  27174  dchrptlem1  27225  bposlem6  27250  gausslemma2dlem0i  27325  gausslemma2dlem1a  27326  lgseisenlem2  27337  2sqlem6  27384  2sq2  27394  2sqnn0  27399  2sqreulem1  27407  2sqreunnlem1  27410  dchrisum0lem1  27477  pntrsumbnd2  27528  pntlem3  27570  noextenddif  27630  nosupno  27665  nosupbnd1  27676  noinfno  27680  noinfbnd1  27691  noetasuplem4  27698  noetainflem4  27702  scutun12  27772  slerec  27781  cutlt  27883  sleadd2im  27938  colinearalg  28835  eengtrkg  28911  incistruhgr  29004  wlkv0  29577  crctcshwlkn0  29749  clwwlkccatlem  29916  clwlkclwwlklem2a4  29924  clwlkclwwlklem2  29927  clwlkclwwlkfo  29936  eucrctshift  30170  frrusgrord0  30267  frgrreg  30321  blocni  30732  ubthlem1  30797  minvecolem4  30807  shmodsi  31316  atcvati  32313  atcvat2i  32314  chirredlem4  32320  atmd2  32327  sumdmdlem  32345  addltmulALT  32373  iundisj2f  32517  iundisj2fi  32720  f1resveqaeq  35062  erdszelem9  35167  satffunlem1lem2  35371  satffunlem2lem2  35374  rdgprc  35758  cgrsub  36009  btwnxfr  36020  lineext  36040  linecgr  36045  btwnconn1lem4  36054  btwnconn1lem5  36055  btwnconn1lem6  36056  btwnconn1lem8  36058  btwnconn1lem11  36061  mptsnunlem  37302  finxpreclem6  37360  ltflcei  37578  poimirlem23  37613  poimirlem24  37614  poimirlem31  37621  poimirlem32  37622  ftc1anclem5  37667  heiborlem6  37786  grpokerinj  37863  dvrunz  37924  isdmn3  38044  dmncan1  38046  membpartlem19  38775  l1cvpat  39018  atnle  39281  cvlexch3  39296  cvlexch4N  39297  cvlatexchb1  39298  cvrat2  39394  atlelt  39403  3dimlem4a  39428  3dimlem4OLDN  39430  ps-1  39442  ps-2  39443  4atlem10  39571  4atlem11  39574  4atlem12  39577  cdleme11c  40226  cdleme21c  40292  cdlemg6d  40586  trlcoat  40688  tendoid0  40790  cdleml3N  40943  dia2dimlem7  41035  aks6d1c6lem3  42131  metakunt1  42164  metakunt6  42169  expeq1d  42320  fsuppind  42560  pellexlem1  42799  pellexlem6  42804  imasgim  43071  onsupmaxb  43210  safesnsupfidom1o  43388  reabsifnpos  43604  reabsifnneg  43606  iunrelexpmin1  43679  iunrelexpmin2  43683  radcnvrat  44286  nzss  44289  pwclaxpow  44957  ormkglobd  46852  elprneb  47006  or2expropbi  47011  tz6.12i-afv2  47220  dfatcolem  47232  f1oresf1o2  47268  zm1nn  47279  2ffzoeq  47304  sfprmdvdsmersenne  47565  lighneallem3  47569  lighneallem4  47572  requad01  47583  fppr2odd  47693  fpprwppr  47701  stgoldbwt  47738  sbgoldbaltlem1  47741  isuspgrimlem  47856  upgrimpthslem2  47869  isubgr3stgrlem4  47929  isubgr3stgrlem7  47932  gpg5nbgrvtx03starlem1  48018  gpg5nbgrvtx03starlem3  48020  gpg5nbgrvtx13starlem1  48021  gpg5nbgrvtx13starlem3  48023  lmod0rng  48152  lidldomn1  48154  rngcisoALTV  48200  ringcisoALTV  48234  ztprmneprm  48270  lincresunit3  48405  itsclc0yqsol  48692  itschlc0xyqsol1  48694  aacllem  49613