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 ⊢ (𝜑 → (𝜓 → 𝜃))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  3imtr3d  296  ceqex  3605  eqreu  3686  sotr2  5589  sotr3  5596  sossfld  6173  ordintdif  6403  tz6.12i  6899  f1cofveqaeqALT  7250  f1resveqaeq  7265  soisoi  7324  riotaeqimp  7391  ov3  7571  tfindsg  7855  tfindsg2  7856  nnsuc  7878  findsg  7892  soseq  8154  suppssr  8190  suppssrg  8191  tfrlem9  8371  oe0lem  8499  oa00  8545  omwordi  8557  om00  8561  omass  8566  oelim2  8582  oeoa  8584  oeoe  8586  nnmwordi  8622  swoso  8730  dom2lem  8997  onsdominel  9123  f1finf1o  9242  fiint  9296  cantnfp1lem3  9659  cantnfp1  9660  cantnflem1  9668  ttrclselem2  9705  rankr1ai  9780  rankval3b  9809  harcard  10031  infxpenlem  10064  alephnbtwn  10122  alephinit  10146  infxp  10264  cofsmo  10319  infpssALT  10363  fin23lem24  10372  fin56  10443  ttukeylem6  10564  ficard  10621  alephval2  10629  fpwwe2lem7  10694  fpwwe2  10700  gchdju1  10713  pwfseqlem3  10717  pwfseqlem4a  10718  pwfseqlem4  10719  gchpwdom  10727  tskss  10815  inar1  10832  gruss  10853  gruurn  10855  ltsonq  11026  distrlem4pr  11083  sqgt0sr  11163  map2psrpr  11167  letric  11382  renegcli  11591  addid0  11705  mulge0b  12157  nnge1  12336  0mnnnnn0  12608  nn0lt2  12732  zneo  12752  uzind2  12762  fzind  12767  nn0ind-raph  12769  uzwo  13008  nn01to3  13038  zbtwnre  13043  rpnnen1lem5  13079  ledivge1le  13163  xrletri  13252  qsqueeze  13301  difreicc  13585  elfzmlbp  13742  difelfznle  13745  elfzodifsumelfzo  13835  ssfzo12  13863  elfzonelfzo  13873  flflp1  13916  fleqceilz  13963  modsumfzodifsn  14056  addmodlteq  14058  om2uzf1oi  14065  expnngt1  14353  facdiv  14399  facwordi  14401  bcpasc  14433  hashdom  14491  hashgt23el  14537  hashdmpropge2  14596  ccatsymb  14696  swrdnnn0nd  14774  swrdnd0  14775  swrdsbslen  14782  swrdspsleq  14783  swrdlsw  14785  pfxnd0  14806  swrdswrdlem  14821  swrdccatin1  14842  pfxccatin12lem3  14849  swrdccat  14852  pfxccat3a  14855  repswswrd  14903  cshwidx0  14925  cshwcsh2id  14947  limsupbnd1  15617  lo1bdd2  15659  addcn2  15729  mulcn2  15731  o1rlimmul  15754  lo1add  15762  lo1mul  15763  rlimno1  15789  ruclem3  16369  odd2np1  16479  oddge22np1  16487  bitsfzo  16573  cncongr1  16805  2mulprm  16831  prm23ge5  16955  pcdvdsb  17009  pcaddlem  17028  infpnlem1  17050  prmunb  17054  vdwlem9  17129  vdwnnlem3  17137  ramcl  17169  prmgaplem5  17195  cshwshash  17244  setcmon  18224  setcepi  18225  setciso  18228  xpsmnd0  18934  f1ghm0to0  19421  ghmf1  19422  sylow2alem2  19794  sylow2blem3  19798  qusabl  20041  lt6abl  20071  cyggexb  20075  gsumcom2  20151  ringurd  20373  imasring  20522  xpsring1d  20525  0ring1eq0  20747  subrgdvds  20800  rngciso  20852  ringciso  20886  isdomn4  20929  drnginvrcl  20973  drnginvrl  20976  drnginvrr  20977  lsmelval2  21322  quscrng  21541  xrsdsreclblem  21681  obs2ss  21997  obslbs  21998  rnasclassa  22165  mplsubrglem  22273  psdmul  22449  gsummoncoe1  22588  mp2pm2mplem4  23089  chfacfisf  23134  chfacfisfcpmat  23135  cayleyhamilton1  23172  cmpsublem  23679  cmpsub  23680  1stccnp  23743  locfincf  23812  txhaus  23928  xkohaus  23934  ufilss  24186  cfinufil  24209  fmfnfmlem1  24235  hausflim  24262  fclscf  24306  alexsubb  24327  qustgplem  24402  prdsbl  24772  metss2lem  24792  nghmcn  25026  cfil3i  25552  cmetcaulem  25571  minveclem4  25715  ovolgelb  25763  ovolunnul  25783  ovoliun  25788  ovoliunnul  25790  ovolicc2lem2  25801  iundisj2  25832  voliunlem3  25835  rolle  26272  dvlip  26275  lhop1lem  26295  lhop2  26297  dvfsumrlim  26313  deg1ge  26378  coeeulem  26505  dgrco  26556  radcnvlt1  26709  psercnlem1  26716  logcnlem2  26935  logcnlem3  26936  cxpeq  27049  angpined  27122  efrlim  27261  dmgmaddn0  27314  lgamucov  27329  basellem2  27373  ppieq0  27467  mumullem2  27471  chpeq0  27499  chteq0  27500  chtub  27503  fsumvma  27504  dchrptlem1  27555  bposlem6  27580  gausslemma2dlem0i  27655  gausslemma2dlem1a  27656  lgseisenlem2  27667  2sqlem6  27714  2sq2  27724  2sqnn0  27729  2sqreulem1  27737  2sqreunnlem1  27740  dchrisum0lem1  27807  pntrsumbnd2  27858  pntlem3  27900  noextenddif  27959  nosupno  27994  nosupbnd1  28005  noinfno  28009  noinfbnd1  28020  noetasuplem4  28027  noetainflem4  28031  cutsun12  28110  lesrec  28119  cutlt  28252  leadds2im  28308  oniso  28591  n0fincut  28675  bdayfinbndlem1  28787  z12bdaylem1  28790  colinearalg  29422  eengtrkg  29498  incistruhgr  29591  wlkv0  30164  crctcshwlkn0  30344  clwwlkccatlem  30514  clwlkclwwlklem2a4  30522  clwlkclwwlklem2  30525  clwlkclwwlkfo  30534  eucrctshift  30778  frrusgrord0  30875  frgrreg  30929  blocni  31341  ubthlem1  31406  minvecolem4  31416  shmodsi  31925  atcvati  32922  atcvat2i  32923  chirredlem4  32929  atmd2  32936  sumdmdlem  32954  addltmulALT  32982  iundisj2f  33118  iundisj2fi  33323  erdszelem9  35885  satffunlem1lem2  36089  satffunlem2lem2  36092  rdgprc  36478  cgrsub  36732  btwnxfr  36743  lineext  36763  linecgr  36768  btwnconn1lem4  36777  btwnconn1lem5  36778  btwnconn1lem6  36779  btwnconn1lem8  36781  btwnconn1lem11  36784  mptsnunlem  38181  finxpreclem6  38239  ltflcei  38451  poimirlem23  38481  poimirlem24  38482  poimirlem31  38489  poimirlem32  38490  ftc1anclem5  38535  heiborlem6  38670  grpokerinj  38747  dvrunz  38808  isdmn3  38928  dmncan1  38930  membpartlem19  39766  l1cvpat  40031  atnle  40294  cvlexch3  40309  cvlexch4N  40310  cvlatexchb1  40311  cvrat2  40406  atlelt  40415  3dimlem4a  40440  3dimlem4OLDN  40442  ps-1  40454  ps-2  40455  4atlem10  40583  4atlem11  40586  4atlem12  40589  cdleme11c  41238  cdleme21c  41304  cdlemg6d  41598  trlcoat  41700  tendoid0  41802  cdleml3N  41955  dia2dimlem7  42047  aks6d1c6lem3  43142  expeq1d  43303  fsuppind  43540  pellexlem1  43774  pellexlem6  43779  imasgim  44045  onsupmaxb  44184  safesnsupfidom1o  44361  reabsifnpos  44577  reabsifnneg  44579  iunrelexpmin1  44652  iunrelexpmin2  44656  radcnvrat  45242  nzss  45245  pwclaxpow  45911  ormkglobd  47809  elprneb  48021  or2expropbi  48026  tz6.12i-afv2  48235  dfatcolem  48247  f1oresf1o2  48283  zm1nn  48294  2ffzoeq  48320  modmkpkne  48359  sfprmdvdsmersenne  48610  lighneallem3  48614  lighneallem4  48617  requad01  48641  fppr2odd  48751  fpprwppr  48759  stgoldbwt  48796  sbgoldbaltlem1  48799  isuspgrimlem  48915  upgrimpthslem2  48928  isubgr3stgrlem4  48989  isubgr3stgrlem7  48992  gpg5nbgrvtx03starlem1  49088  gpg5nbgrvtx03starlem3  49090  gpg5nbgrvtx13starlem1  49091  gpg5nbgrvtx13starlem3  49093  lmod0rng  49248  lidldomn1  49250  rngcisoALTV  49296  ringcisoALTV  49330  isidom3  49364  idomcanl  49366  ztprmneprm  49381  lincresunit3  49515  itsclc0yqsol  49798  itschlc0xyqsol1  49800  aacllem  50861