Theorem sylbird 259

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  292  ceqex  3605  eqreu  3690  sotr2  5582  sotr3  5589  sossfld  6143  ordintdif  6372  tz6.12i  6875  f1cofveqaeqALT  7211  soisoi  7278  riotaeqimp  7345  ov3  7522  tfindsg  7802  tfindsg2  7803  nnsuc  7825  findsg  7841  soseq  8096  suppssr  8132  suppssrg  8133  tfrlem9  8336  oe0lem  8464  oa00  8511  omwordi  8523  om00  8527  omass  8532  oelim2  8547  oeoa  8549  oeoe  8551  nnmwordi  8587  swoso  8688  dom2lem  8939  onsdominel  9077  f1finf1o  9222  f1finf1oOLD  9223  cantnfp1lem3  9625  cantnfp1  9626  cantnflem1  9634  ttrclselem2  9671  rankr1ai  9743  rankval3b  9771  harcard  9923  infxpenlem  9958  alephnbtwn  10016  alephinit  10040  infxp  10160  cofsmo  10214  infpssALT  10258  fin23lem24  10267  fin56  10338  ttukeylem6  10459  ficard  10510  alephval2  10517  fpwwe2lem7  10582  fpwwe2  10588  gchdju1  10601  pwfseqlem3  10605  pwfseqlem4a  10606  pwfseqlem4  10607  gchpwdom  10615  tskss  10703  inar1  10720  gruss  10741  gruurn  10743  ltsonq  10914  distrlem4pr  10971  sqgt0sr  11051  map2psrpr  11055  letric  11264  renegcli  11471  addid0  11583  mulge0b  12034  nnge1  12190  0mnnnnn0  12454  nn0lt2  12575  zneo  12595  uzind2  12605  fzind  12610  nn0ind-raph  12612  uzwo  12845  nn01to3  12875  zbtwnre  12880  rpnnen1lem5  12915  ledivge1le  12995  xrletri  13082  qsqueeze  13130  difreicc  13411  elfzmlbp  13562  difelfznle  13565  elfzodifsumelfzo  13648  ssfzo12  13675  elfzonelfzo  13684  flflp1  13722  fleqceilz  13769  modsumfzodifsn  13859  addmodlteq  13861  om2uzf1oi  13868  expnngt1  14154  facdiv  14197  facwordi  14199  bcpasc  14231  hashdom  14289  hashgt23el  14334  hashdmpropge2  14394  ccatsymb  14482  swrdnnn0nd  14556  swrdnd0  14557  swrdsbslen  14564  swrdspsleq  14565  swrdlsw  14567  pfxnd0  14588  swrdswrdlem  14604  swrdccatin1  14625  pfxccatin12lem3  14632  swrdccat  14635  pfxccat3a  14638  repswswrd  14684  cshwidx0  14706  cshwcsh2id  14729  limsupbnd1  15376  lo1bdd2  15418  addcn2  15488  mulcn2  15490  o1rlimmul  15513  lo1add  15521  lo1mul  15522  rlimno1  15550  ruclem3  16126  odd2np1  16234  oddge22np1  16242  bitsfzo  16326  cncongr1  16554  2mulprm  16580  prm23ge5  16698  pcdvdsb  16752  pcaddlem  16771  infpnlem1  16793  prmunb  16797  vdwlem9  16872  vdwnnlem3  16880  ramcl  16912  prmgaplem5  16938  cshwshash  16988  setcmon  17987  setcepi  17988  setciso  17991  ghmf1  19051  sylow2alem2  19414  sylow2blem3  19418  qusabl  19657  lt6abl  19686  cyggexb  19690  gsumcom2  19766  imasring  20059  f1ghm0to0  20190  drnginvrcl  20246  drnginvrl  20249  drnginvrr  20250  subrgdvds  20284  lsmelval2  20603  quscrng  20769  xrsdsreclblem  20880  obs2ss  21172  obslbs  21173  rnasclassa  21335  mplsubrglem  21447  gsummoncoe1  21712  mp2pm2mplem4  22195  chfacfisf  22240  chfacfisfcpmat  22241  cayleyhamilton1  22278  cmpsublem  22787  cmpsub  22788  1stccnp  22850  locfincf  22919  txhaus  23035  xkohaus  23041  ufilss  23293  cfinufil  23316  fmfnfmlem1  23342  hausflim  23369  fclscf  23413  alexsubb  23434  qustgplem  23509  prdsbl  23884  metss2lem  23904  nghmcn  24146  cfil3i  24670  cmetcaulem  24689  minveclem4  24833  ovolgelb  24881  ovolunnul  24901  ovoliun  24906  ovoliunnul  24908  ovolicc2lem2  24919  iundisj2  24950  voliunlem3  24953  rolle  25391  dvlip  25394  lhop1lem  25414  lhop2  25416  dvfsumrlim  25432  deg1ge  25500  coeeulem  25622  dgrco  25673  radcnvlt1  25814  psercnlem1  25821  logcnlem2  26035  logcnlem3  26036  cxpeq  26147  angpined  26217  efrlim  26356  dmgmaddn0  26409  lgamucov  26424  basellem2  26468  ppieq0  26562  mumullem2  26566  chpeq0  26593  chteq0  26594  chtub  26597  fsumvma  26598  dchrptlem1  26649  bposlem6  26674  gausslemma2dlem0i  26749  gausslemma2dlem1a  26750  lgseisenlem2  26761  2sqlem6  26808  2sq2  26818  2sqnn0  26823  2sqreulem1  26831  2sqreunnlem1  26834  dchrisum0lem1  26901  pntrsumbnd2  26952  pntlem3  26994  noextenddif  27053  nosupno  27088  nosupbnd1  27099  noinfno  27103  noinfbnd1  27114  noetasuplem4  27121  noetainflem4  27125  scutun12  27192  slerec  27201  sleadd2im  27340  colinearalg  27922  eengtrkg  27998  incistruhgr  28093  wlkv0  28662  crctcshwlkn0  28829  clwwlkccatlem  28996  clwlkclwwlklem2a4  29004  clwlkclwwlklem2  29007  clwlkclwwlkfo  29016  eucrctshift  29250  frrusgrord0  29347  frgrreg  29401  blocni  29810  ubthlem1  29875  minvecolem4  29885  shmodsi  30394  atcvati  31391  atcvat2i  31392  chirredlem4  31398  atmd2  31405  sumdmdlem  31423  addltmulALT  31451  iundisj2f  31575  iundisj2fi  31768  rngurd  32135  f1resveqaeq  33778  erdszelem9  33880  satffunlem1lem2  34084  satffunlem2lem2  34087  rdgprc  34455  cgrsub  34706  btwnxfr  34717  lineext  34737  linecgr  34742  btwnconn1lem4  34751  btwnconn1lem5  34752  btwnconn1lem6  34753  btwnconn1lem8  34755  btwnconn1lem11  34758  mptsnunlem  35882  finxpreclem6  35940  ltflcei  36139  poimirlem23  36174  poimirlem24  36175  poimirlem31  36182  poimirlem32  36183  ftc1anclem5  36228  heiborlem6  36348  grpokerinj  36425  dvrunz  36486  isdmn3  36606  dmncan1  36608  membpartlem19  37346  l1cvpat  37589  atnle  37852  cvlexch3  37867  cvlexch4N  37868  cvlatexchb1  37869  cvrat2  37965  atlelt  37974  3dimlem4a  37999  3dimlem4OLDN  38001  ps-1  38013  ps-2  38014  4atlem10  38142  4atlem11  38145  4atlem12  38148  cdleme11c  38797  cdleme21c  38863  cdlemg6d  39157  trlcoat  39259  tendoid0  39361  cdleml3N  39514  dia2dimlem7  39606  metakunt1  40650  metakunt6  40655  isdomn4  40697  fsuppind  40823  pellexlem1  41210  pellexlem6  41215  imasgim  41485  onsupmaxb  41631  safesnsupfidom1o  41811  reabsifnpos  42027  reabsifnneg  42029  iunrelexpmin1  42102  iunrelexpmin2  42106  radcnvrat  42716  nzss  42719  elprneb  45383  or2expropbi  45388  tz6.12i-afv2  45595  dfatcolem  45607  f1oresf1o2  45643  zm1nn  45654  2ffzoeq  45680  sfprmdvdsmersenne  45915  lighneallem3  45919  lighneallem4  45922  requad01  45933  fppr2odd  46043  fpprwppr  46051  stgoldbwt  46088  sbgoldbaltlem1  46091  isomuspgrlem1  46139  lmod0rng  46286  0ring1eq0  46290  lidldomn1  46339  rngciso  46400  rngcisoALTV  46412  ringciso  46451  ringcisoALTV  46475  ztprmneprm  46543  lincresunit3  46682  itsclc0yqsol  46970  itschlc0xyqsol1  46972  aacllem  47368