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  3610  eqreu  3691  sotr2  5602  sotr3  5609  sossfld  6183  ordintdif  6412  tz6.12i  6907  f1cofveqaeqALT  7256  soisoi  7326  riotaeqimp  7395  ov3  7575  tfindsg  7855  tfindsg2  7856  nnsuc  7878  findsg  7892  soseq  8153  suppssr  8189  suppssrg  8190  tfrlem9  8370  oe0lem  8496  oa00  8542  omwordi  8554  om00  8558  omass  8563  oelim2  8579  oeoa  8581  oeoe  8583  nnmwordi  8619  swoso  8727  dom2lem  8987  onsdominel  9112  f1finf1o  9231  fiint  9284  cantnfp1lem3  9647  cantnfp1  9648  cantnflem1  9656  ttrclselem2  9693  rankr1ai  9768  rankval3b  9796  harcard  9971  infxpenlem  10004  alephnbtwn  10062  alephinit  10086  infxp  10204  cofsmo  10259  infpssALT  10303  fin23lem24  10312  fin56  10383  ttukeylem6  10504  ficard  10555  alephval2  10563  fpwwe2lem7  10628  fpwwe2  10634  gchdju1  10647  pwfseqlem3  10651  pwfseqlem4a  10652  pwfseqlem4  10653  gchpwdom  10661  tskss  10749  inar1  10766  gruss  10787  gruurn  10789  ltsonq  10960  distrlem4pr  11017  sqgt0sr  11097  map2psrpr  11101  letric  11316  renegcli  11525  addid0  11639  mulge0b  12091  nnge1  12270  0mnnnnn0  12542  nn0lt2  12665  zneo  12685  uzind2  12695  fzind  12700  nn0ind-raph  12702  uzwo  12941  nn01to3  12971  zbtwnre  12976  rpnnen1lem5  13011  ledivge1le  13095  xrletri  13184  qsqueeze  13233  difreicc  13517  elfzmlbp  13674  difelfznle  13677  elfzodifsumelfzo  13767  ssfzo12  13795  elfzonelfzo  13805  flflp1  13847  fleqceilz  13894  modsumfzodifsn  13987  addmodlteq  13989  om2uzf1oi  13996  expnngt1  14284  facdiv  14330  facwordi  14332  bcpasc  14364  hashdom  14422  hashgt23el  14468  hashdmpropge2  14527  ccatsymb  14627  swrdnnn0nd  14701  swrdnd0  14702  swrdsbslen  14709  swrdspsleq  14710  swrdlsw  14712  pfxnd0  14733  swrdswrdlem  14748  swrdccatin1  14769  pfxccatin12lem3  14776  swrdccat  14779  pfxccat3a  14782  repswswrd  14828  cshwidx0  14850  cshwcsh2id  14872  limsupbnd1  15540  lo1bdd2  15582  addcn2  15652  mulcn2  15654  o1rlimmul  15677  lo1add  15685  lo1mul  15686  rlimno1  15712  ruclem3  16295  odd2np1  16405  oddge22np1  16413  bitsfzo  16499  cncongr1  16731  2mulprm  16757  prm23ge5  16881  pcdvdsb  16935  pcaddlem  16954  infpnlem1  16976  prmunb  16980  vdwlem9  17055  vdwnnlem3  17063  ramcl  17095  prmgaplem5  17121  cshwshash  17170  setcmon  18150  setcepi  18151  setciso  18154  xpsmnd0  18842  f1ghm0to0  19321  ghmf1  19322  sylow2alem2  19694  sylow2blem3  19698  qusabl  19941  lt6abl  19971  cyggexb  19975  gsumcom2  20051  ringurd  20273  imasring  20419  xpsring1d  20422  0ring1eq0  20643  subrgdvds  20696  rngciso  20748  ringciso  20782  isdomn4  20825  drnginvrcl  20868  drnginvrl  20871  drnginvrr  20872  lsmelval2  21217  quscrng  21434  xrsdsreclblem  21574  obs2ss  21890  obslbs  21891  rnasclassa  22056  mplsubrglem  22164  psdmul  22340  gsummoncoe1  22479  mp2pm2mplem4  22977  chfacfisf  23022  chfacfisfcpmat  23023  cayleyhamilton1  23060  cmpsublem  23567  cmpsub  23568  1stccnp  23630  locfincf  23699  txhaus  23815  xkohaus  23821  ufilss  24073  cfinufil  24096  fmfnfmlem1  24122  hausflim  24149  fclscf  24193  alexsubb  24214  qustgplem  24289  prdsbl  24659  metss2lem  24679  nghmcn  24913  cfil3i  25439  cmetcaulem  25458  minveclem4  25602  ovolgelb  25650  ovolunnul  25670  ovoliun  25675  ovoliunnul  25677  ovolicc2lem2  25688  iundisj2  25719  voliunlem3  25722  rolle  26160  dvlip  26163  lhop1lem  26183  lhop2  26185  dvfsumrlim  26201  deg1ge  26266  coeeulem  26392  dgrco  26443  radcnvlt1  26592  psercnlem1  26599  logcnlem2  26819  logcnlem3  26820  cxpeq  26933  angpined  27006  efrlim  27145  dmgmaddn0  27198  lgamucov  27213  basellem2  27257  ppieq0  27351  mumullem2  27355  chpeq0  27383  chteq0  27384  chtub  27387  fsumvma  27388  dchrptlem1  27439  bposlem6  27464  gausslemma2dlem0i  27539  gausslemma2dlem1a  27540  lgseisenlem2  27551  2sqlem6  27598  2sq2  27608  2sqnn0  27613  2sqreulem1  27621  2sqreunnlem1  27624  dchrisum0lem1  27691  pntrsumbnd2  27742  pntlem3  27784  noextenddif  27843  nosupno  27878  nosupbnd1  27889  noinfno  27893  noinfbnd1  27904  noetasuplem4  27911  noetainflem4  27915  cutsun12  27994  lesrec  28003  cutlt  28136  leadds2im  28192  oniso  28475  n0fincut  28559  bdayfinbndlem1  28671  z12bdaylem1  28674  colinearalg  29271  eengtrkg  29347  incistruhgr  29440  wlkv0  30010  crctcshwlkn0  30181  clwwlkccatlem  30351  clwlkclwwlklem2a4  30359  clwlkclwwlklem2  30362  clwlkclwwlkfo  30371  eucrctshift  30605  frrusgrord0  30702  frgrreg  30756  blocni  31168  ubthlem1  31233  minvecolem4  31243  shmodsi  31752  atcvati  32749  atcvat2i  32750  chirredlem4  32756  atmd2  32763  sumdmdlem  32781  addltmulALT  32809  iundisj2f  32946  iundisj2fi  33153  f1resveqaeq  35482  erdszelem9  35699  satffunlem1lem2  35903  satffunlem2lem2  35906  rdgprc  36292  cgrsub  36545  btwnxfr  36556  lineext  36576  linecgr  36581  btwnconn1lem4  36590  btwnconn1lem5  36591  btwnconn1lem6  36592  btwnconn1lem8  36594  btwnconn1lem11  36597  mh-inf3f1  37080  mptsnunlem  38012  finxpreclem6  38070  ltflcei  38287  poimirlem23  38322  poimirlem24  38323  poimirlem31  38330  poimirlem32  38331  ftc1anclem5  38376  heiborlem6  38495  grpokerinj  38572  dvrunz  38633  isdmn3  38753  dmncan1  38755  membpartlem19  39591  l1cvpat  39856  atnle  40119  cvlexch3  40134  cvlexch4N  40135  cvlatexchb1  40136  cvrat2  40231  atlelt  40240  3dimlem4a  40265  3dimlem4OLDN  40267  ps-1  40279  ps-2  40280  4atlem10  40408  4atlem11  40411  4atlem12  40414  cdleme11c  41063  cdleme21c  41129  cdlemg6d  41423  trlcoat  41525  tendoid0  41627  cdleml3N  41780  dia2dimlem7  41872  aks6d1c6lem3  42967  expeq1d  43113  fsuppind  43350  pellexlem1  43584  pellexlem6  43589  imasgim  43855  onsupmaxb  43994  safesnsupfidom1o  44171  reabsifnpos  44387  reabsifnneg  44389  iunrelexpmin1  44462  iunrelexpmin2  44466  radcnvrat  45052  nzss  45055  pwclaxpow  45721  ormkglobd  47619  elprneb  47794  or2expropbi  47799  tz6.12i-afv2  48008  dfatcolem  48020  f1oresf1o2  48056  zm1nn  48067  2ffzoeq  48093  modmkpkne  48132  sfprmdvdsmersenne  48383  lighneallem3  48387  lighneallem4  48390  requad01  48414  fppr2odd  48524  fpprwppr  48532  stgoldbwt  48569  sbgoldbaltlem1  48572  isuspgrimlem  48688  upgrimpthslem2  48701  isubgr3stgrlem4  48762  isubgr3stgrlem7  48765  gpg5nbgrvtx03starlem1  48861  gpg5nbgrvtx03starlem3  48863  gpg5nbgrvtx13starlem1  48864  gpg5nbgrvtx13starlem3  48866  lmod0rng  49022  lidldomn1  49024  rngcisoALTV  49070  ringcisoALTV  49104  isidom3  49138  idomcanl  49140  ztprmneprm  49155  lincresunit3  49289  itsclc0yqsol  49572  itschlc0xyqsol1  49574  aacllem  50649