Theorem sylbird 263

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 251	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
3		sylbird.2	. 2 ⊢ (𝜑 → (𝜒 → 𝜃))
4	2, 3	syld 48	1 ⊢ (𝜑 → (𝜓 → 𝜃))

Syntax hints:   → wi 4   ↔ wb 209

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 210

This theorem is referenced by:  3imtr3d  296  ceqex  3614  eqreu  3695  sotr2  5594  sotr3  5601  sossfld  6176  ordintdif  6401  tz6.12i  6897  f1cofveqaeqALT  7246  soisoi  7316  riotaeqimp  7383  ov3  7563  tfindsg  7845  tfindsg2  7846  nnsuc  7868  findsg  7882  soseq  8143  suppssr  8179  suppssrg  8180  tfrlem9  8360  oe0lem  8486  oa00  8532  omwordi  8544  om00  8548  omass  8553  oelim2  8569  oeoa  8571  oeoe  8573  nnmwordi  8609  swoso  8717  dom2lem  8977  onsdominel  9102  f1finf1o  9221  fiint  9274  cantnfp1lem3  9637  cantnfp1  9638  cantnflem1  9646  ttrclselem2  9683  rankr1ai  9758  rankval3b  9786  harcard  9952  infxpenlem  9985  alephnbtwn  10043  alephinit  10067  infxp  10185  cofsmo  10241  infpssALT  10285  fin23lem24  10294  fin56  10365  ttukeylem6  10486  ficard  10537  alephval2  10545  fpwwe2lem7  10610  fpwwe2  10616  gchdju1  10629  pwfseqlem3  10633  pwfseqlem4a  10634  pwfseqlem4  10635  gchpwdom  10643  tskss  10731  inar1  10748  gruss  10769  gruurn  10771  ltsonq  10942  distrlem4pr  10999  sqgt0sr  11079  map2psrpr  11083  letric  11298  renegcli  11507  addid0  11621  mulge0b  12076  nnge1  12255  0mnnnnn0  12527  nn0lt2  12650  zneo  12670  uzind2  12680  fzind  12685  nn0ind-raph  12687  uzwo  12926  nn01to3  12956  zbtwnre  12961  rpnnen1lem5  12996  ledivge1le  13080  xrletri  13169  qsqueeze  13218  difreicc  13502  elfzmlbp  13658  difelfznle  13661  elfzodifsumelfzo  13751  ssfzo12  13779  elfzonelfzo  13789  flflp1  13831  fleqceilz  13878  modsumfzodifsn  13971  addmodlteq  13973  om2uzf1oi  13980  expnngt1  14268  facdiv  14314  facwordi  14316  bcpasc  14348  hashdom  14406  hashgt23el  14451  hashdmpropge2  14510  ccatsymb  14610  swrdnnn0nd  14684  swrdnd0  14685  swrdsbslen  14692  swrdspsleq  14693  swrdlsw  14695  pfxnd0  14716  swrdswrdlem  14731  swrdccatin1  14752  pfxccatin12lem3  14759  swrdccat  14762  pfxccat3a  14765  repswswrd  14811  cshwidx0  14833  cshwcsh2id  14855  limsupbnd1  15523  lo1bdd2  15565  addcn2  15635  mulcn2  15637  o1rlimmul  15660  lo1add  15668  lo1mul  15669  rlimno1  15695  ruclem3  16279  odd2np1  16389  oddge22np1  16397  bitsfzo  16483  cncongr1  16715  2mulprm  16741  prm23ge5  16865  pcdvdsb  16919  pcaddlem  16938  infpnlem1  16960  prmunb  16964  vdwlem9  17039  vdwnnlem3  17047  ramcl  17079  prmgaplem5  17105  cshwshash  17154  setcmon  18134  setcepi  18135  setciso  18138  xpsmnd0  18826  f1ghm0to0  19306  ghmf1  19307  sylow2alem2  19679  sylow2blem3  19683  qusabl  19926  lt6abl  19956  cyggexb  19960  gsumcom2  20036  ringurd  20258  imasring  20403  xpsring1d  20406  0ring1eq0  20609  subrgdvds  20662  rngciso  20714  ringciso  20748  isdomn4  20791  drnginvrcl  20827  drnginvrl  20830  drnginvrr  20831  lsmelval2  21175  quscrng  21385  xrsdsreclblem  21523  obs2ss  21839  obslbs  21840  rnasclassa  22005  mplsubrglem  22113  psdmul  22289  gsummoncoe1  22429  mp2pm2mplem4  22927  chfacfisf  22972  chfacfisfcpmat  22973  cayleyhamilton1  23010  cmpsublem  23517  cmpsub  23518  1stccnp  23580  locfincf  23649  txhaus  23765  xkohaus  23771  ufilss  24023  cfinufil  24046  fmfnfmlem1  24072  hausflim  24099  fclscf  24143  alexsubb  24164  qustgplem  24239  prdsbl  24609  metss2lem  24629  nghmcn  24863  cfil3i  25389  cmetcaulem  25408  minveclem4  25552  ovolgelb  25600  ovolunnul  25620  ovoliun  25625  ovoliunnul  25627  ovolicc2lem2  25638  iundisj2  25669  voliunlem3  25672  rolle  26110  dvlip  26113  lhop1lem  26133  lhop2  26135  dvfsumrlim  26151  deg1ge  26216  coeeulem  26342  dgrco  26393  radcnvlt1  26539  psercnlem1  26546  logcnlem2  26766  logcnlem3  26767  cxpeq  26880  angpined  26953  efrlim  27092  dmgmaddn0  27145  lgamucov  27160  basellem2  27204  ppieq0  27298  mumullem2  27302  chpeq0  27330  chteq0  27331  chtub  27334  fsumvma  27335  dchrptlem1  27386  bposlem6  27411  gausslemma2dlem0i  27486  gausslemma2dlem1a  27487  lgseisenlem2  27498  2sqlem6  27545  2sq2  27555  2sqnn0  27560  2sqreulem1  27568  2sqreunnlem1  27571  dchrisum0lem1  27638  pntrsumbnd2  27689  pntlem3  27731  noextenddif  27790  nosupno  27825  nosupbnd1  27836  noinfno  27840  noinfbnd1  27851  noetasuplem4  27858  noetainflem4  27862  cutsun12  27941  lesrec  27950  cutlt  28083  leadds2im  28139  oniso  28422  n0fincut  28506  bdayfinbndlem1  28618  z12bdaylem1  28621  colinearalg  29169  eengtrkg  29245  incistruhgr  29338  wlkv0  29908  crctcshwlkn0  30079  clwwlkccatlem  30249  clwlkclwwlklem2a4  30257  clwlkclwwlklem2  30260  clwlkclwwlkfo  30269  eucrctshift  30503  frrusgrord0  30600  frgrreg  30654  blocni  31066  ubthlem1  31131  minvecolem4  31141  shmodsi  31650  atcvati  32647  atcvat2i  32648  chirredlem4  32654  atmd2  32661  sumdmdlem  32679  addltmulALT  32707  iundisj2f  32845  iundisj2fi  33054  f1resveqaeq  35389  erdszelem9  35562  satffunlem1lem2  35766  satffunlem2lem2  35769  rdgprc  36155  cgrsub  36408  btwnxfr  36419  lineext  36439  linecgr  36444  btwnconn1lem4  36453  btwnconn1lem5  36454  btwnconn1lem6  36455  btwnconn1lem8  36457  btwnconn1lem11  36460  mh-inf3f1  36914  mptsnunlem  37844  finxpreclem6  37902  ltflcei  38119  poimirlem23  38154  poimirlem24  38155  poimirlem31  38162  poimirlem32  38163  ftc1anclem5  38208  heiborlem6  38327  grpokerinj  38404  dvrunz  38465  isdmn3  38585  dmncan1  38587  membpartlem19  39425  l1cvpat  39690  atnle  39953  cvlexch3  39968  cvlexch4N  39969  cvlatexchb1  39970  cvrat2  40065  atlelt  40074  3dimlem4a  40099  3dimlem4OLDN  40101  ps-1  40113  ps-2  40114  4atlem10  40242  4atlem11  40245  4atlem12  40248  cdleme11c  40897  cdleme21c  40963  cdlemg6d  41257  trlcoat  41359  tendoid0  41461  cdleml3N  41614  dia2dimlem7  41706  aks6d1c6lem3  42801  expeq1d  42945  fsuppind  43184  pellexlem1  43418  pellexlem6  43423  imasgim  43689  onsupmaxb  43828  safesnsupfidom1o  44005  reabsifnpos  44221  reabsifnneg  44223  iunrelexpmin1  44296  iunrelexpmin2  44300  radcnvrat  44888  nzss  44891  pwclaxpow  45558  ormkglobd  47449  elprneb  47621  or2expropbi  47626  tz6.12i-afv2  47835  dfatcolem  47847  f1oresf1o2  47883  zm1nn  47894  2ffzoeq  47920  modmkpkne  47959  sfprmdvdsmersenne  48210  lighneallem3  48214  lighneallem4  48217  requad01  48241  fppr2odd  48351  fpprwppr  48359  stgoldbwt  48396  sbgoldbaltlem1  48399  isuspgrimlem  48515  upgrimpthslem2  48528  isubgr3stgrlem4  48589  isubgr3stgrlem7  48592  gpg5nbgrvtx03starlem1  48688  gpg5nbgrvtx03starlem3  48690  gpg5nbgrvtx13starlem1  48691  gpg5nbgrvtx13starlem3  48693  lmod0rng  48849  lidldomn1  48851  rngcisoALTV  48897  ringcisoALTV  48931  ztprmneprm  48978  lincresunit3  49112  itsclc0yqsol  49395  itschlc0xyqsol1  49397  aacllem  50430