Theorem sylbird 261

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

Syntax hints:   → wi 4   ↔ wb 207

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 208

This theorem is referenced by:  3imtr3d  294  ceqex  3597  eqreu  3677  sotr2  5567  sotr3  5574  sossfld  6144  ordintdif  6368  tz6.12i  6860  f1cofveqaeqALT  7209  soisoi  7279  riotaeqimp  7346  ov3  7526  tfindsg  7808  tfindsg2  7809  nnsuc  7831  findsg  7844  soseq  8106  suppssr  8142  suppssrg  8143  tfrlem9  8321  oe0lem  8445  oa00  8491  omwordi  8503  om00  8507  omass  8512  oelim2  8528  oeoa  8530  oeoe  8532  nnmwordi  8568  swoso  8675  dom2lem  8936  onsdominel  9061  f1finf1o  9180  fiint  9234  cantnfp1lem3  9599  cantnfp1  9600  cantnflem1  9608  ttrclselem2  9645  rankr1ai  9720  rankval3b  9748  harcard  9900  infxpenlem  9933  alephnbtwn  9991  alephinit  10015  infxp  10134  cofsmo  10189  infpssALT  10233  fin23lem24  10242  fin56  10313  ttukeylem6  10434  ficard  10485  alephval2  10493  fpwwe2lem7  10558  fpwwe2  10564  gchdju1  10577  pwfseqlem3  10581  pwfseqlem4a  10582  pwfseqlem4  10583  gchpwdom  10591  tskss  10679  inar1  10696  gruss  10717  gruurn  10719  ltsonq  10890  distrlem4pr  10947  sqgt0sr  11027  map2psrpr  11031  letric  11244  renegcli  11453  addid0  11567  mulge0b  12024  nnge1  12203  0mnnnnn0  12467  nn0lt2  12590  zneo  12610  uzind2  12620  fzind  12625  nn0ind-raph  12627  uzwo  12859  nn01to3  12889  zbtwnre  12894  rpnnen1lem5  12929  ledivge1le  13013  xrletri  13102  qsqueeze  13151  difreicc  13435  elfzmlbp  13591  difelfznle  13594  elfzodifsumelfzo  13684  ssfzo12  13712  elfzonelfzo  13722  flflp1  13764  fleqceilz  13811  modsumfzodifsn  13904  addmodlteq  13906  om2uzf1oi  13913  expnngt1  14201  facdiv  14247  facwordi  14249  bcpasc  14281  hashdom  14339  hashgt23el  14384  hashdmpropge2  14443  ccatsymb  14543  swrdnnn0nd  14617  swrdnd0  14618  swrdsbslen  14625  swrdspsleq  14626  swrdlsw  14628  pfxnd0  14649  swrdswrdlem  14664  swrdccatin1  14685  pfxccatin12lem3  14692  swrdccat  14695  pfxccat3a  14698  repswswrd  14744  cshwidx0  14766  cshwcsh2id  14788  limsupbnd1  15442  lo1bdd2  15484  addcn2  15554  mulcn2  15556  o1rlimmul  15579  lo1add  15587  lo1mul  15588  rlimno1  15614  ruclem3  16198  odd2np1  16308  oddge22np1  16316  bitsfzo  16402  cncongr1  16634  2mulprm  16660  prm23ge5  16784  pcdvdsb  16838  pcaddlem  16857  infpnlem1  16879  prmunb  16883  vdwlem9  16958  vdwnnlem3  16966  ramcl  16998  prmgaplem5  17024  cshwshash  17073  setcmon  18052  setcepi  18053  setciso  18056  xpsmnd0  18744  f1ghm0to0  19218  ghmf1  19219  sylow2alem2  19591  sylow2blem3  19595  qusabl  19838  lt6abl  19868  cyggexb  19872  gsumcom2  19948  ringurd  20164  imasring  20308  xpsring1d  20311  0ring1eq0  20512  subrgdvds  20565  rngciso  20617  ringciso  20651  isdomn4  20695  drnginvrcl  20732  drnginvrl  20735  drnginvrr  20736  lsmelval2  21082  quscrng  21283  xrsdsreclblem  21395  obs2ss  21711  obslbs  21712  rnasclassa  21877  mplsubrglem  21985  psdmul  22161  gsummoncoe1  22301  mp2pm2mplem4  22799  chfacfisf  22844  chfacfisfcpmat  22845  cayleyhamilton1  22882  cmpsublem  23389  cmpsub  23390  1stccnp  23452  locfincf  23521  txhaus  23637  xkohaus  23643  ufilss  23895  cfinufil  23918  fmfnfmlem1  23944  hausflim  23971  fclscf  24015  alexsubb  24036  qustgplem  24111  prdsbl  24481  metss2lem  24501  nghmcn  24735  cfil3i  25261  cmetcaulem  25280  minveclem4  25424  ovolgelb  25472  ovolunnul  25492  ovoliun  25497  ovoliunnul  25499  ovolicc2lem2  25510  iundisj2  25541  voliunlem3  25544  rolle  25982  dvlip  25985  lhop1lem  26005  lhop2  26007  dvfsumrlim  26023  deg1ge  26088  coeeulem  26214  dgrco  26265  radcnvlt1  26408  psercnlem1  26415  logcnlem2  26632  logcnlem3  26633  cxpeq  26746  angpined  26819  efrlim  26958  dmgmaddn0  27011  lgamucov  27026  basellem2  27070  ppieq0  27164  mumullem2  27168  chpeq0  27196  chteq0  27197  chtub  27200  fsumvma  27201  dchrptlem1  27252  bposlem6  27277  gausslemma2dlem0i  27352  gausslemma2dlem1a  27353  lgseisenlem2  27364  2sqlem6  27411  2sq2  27421  2sqnn0  27426  2sqreulem1  27434  2sqreunnlem1  27437  dchrisum0lem1  27504  pntrsumbnd2  27555  pntlem3  27597  noextenddif  27657  nosupno  27692  nosupbnd1  27703  noinfno  27707  noinfbnd1  27718  noetasuplem4  27725  noetainflem4  27729  cutsun12  27807  lesrec  27816  cutlt  27949  leadds2im  28005  oniso  28288  n0fincut  28372  bdayfinbndlem1  28484  z12bdaylem1  28487  colinearalg  29004  eengtrkg  29080  incistruhgr  29173  wlkv0  29743  crctcshwlkn0  29914  clwwlkccatlem  30084  clwlkclwwlklem2a4  30092  clwlkclwwlklem2  30095  clwlkclwwlkfo  30104  eucrctshift  30338  frrusgrord0  30435  frgrreg  30489  blocni  30901  ubthlem1  30966  minvecolem4  30976  shmodsi  31485  atcvati  32482  atcvat2i  32483  chirredlem4  32489  atmd2  32496  sumdmdlem  32514  addltmulALT  32542  iundisj2f  32686  iundisj2fi  32896  f1resveqaeq  35275  erdszelem9  35428  satffunlem1lem2  35632  satffunlem2lem2  35635  rdgprc  36021  cgrsub  36274  btwnxfr  36285  lineext  36305  linecgr  36310  btwnconn1lem4  36319  btwnconn1lem5  36320  btwnconn1lem6  36321  btwnconn1lem8  36323  btwnconn1lem11  36326  mh-inf3f1  36770  mptsnunlem  37701  finxpreclem6  37759  ltflcei  37976  poimirlem23  38011  poimirlem24  38012  poimirlem31  38019  poimirlem32  38020  ftc1anclem5  38065  heiborlem6  38184  grpokerinj  38261  dvrunz  38322  isdmn3  38442  dmncan1  38444  membpartlem19  39282  l1cvpat  39547  atnle  39810  cvlexch3  39825  cvlexch4N  39826  cvlatexchb1  39827  cvrat2  39922  atlelt  39931  3dimlem4a  39956  3dimlem4OLDN  39958  ps-1  39970  ps-2  39971  4atlem10  40099  4atlem11  40102  4atlem12  40105  cdleme11c  40754  cdleme21c  40820  cdlemg6d  41114  trlcoat  41216  tendoid0  41318  cdleml3N  41471  dia2dimlem7  41563  aks6d1c6lem3  42658  expeq1d  42802  fsuppind  43041  pellexlem1  43275  pellexlem6  43280  imasgim  43546  onsupmaxb  43685  safesnsupfidom1o  43862  reabsifnpos  44078  reabsifnneg  44080  iunrelexpmin1  44153  iunrelexpmin2  44157  radcnvrat  44759  nzss  44762  pwclaxpow  45429  ormkglobd  47321  elprneb  47493  or2expropbi  47498  tz6.12i-afv2  47707  dfatcolem  47719  f1oresf1o2  47755  zm1nn  47766  2ffzoeq  47792  modmkpkne  47831  sfprmdvdsmersenne  48082  lighneallem3  48086  lighneallem4  48089  requad01  48113  fppr2odd  48223  fpprwppr  48231  stgoldbwt  48268  sbgoldbaltlem1  48271  isuspgrimlem  48387  upgrimpthslem2  48400  isubgr3stgrlem4  48461  isubgr3stgrlem7  48464  gpg5nbgrvtx03starlem1  48560  gpg5nbgrvtx03starlem3  48562  gpg5nbgrvtx13starlem1  48563  gpg5nbgrvtx13starlem3  48565  lmod0rng  48721  lidldomn1  48723  rngcisoALTV  48769  ringcisoALTV  48803  ztprmneprm  48839  lincresunit3  48973  itsclc0yqsol  49256  itschlc0xyqsol1  49258  aacllem  50292