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  3609  eqreu  3690  sotr2  5597  sotr3  5604  sossfld  6190  ordintdif  6432  tz6.12i  6934  f1cofveqaeqALT  7285  f1resveqaeq  7300  soisoi  7359  riotaeqimp  7426  ov3  7607  tfindsg  7896  tfindsg2  7897  nnsuc  7919  findsg  7933  soseq  8203  suppssr  8240  suppssrg  8241  tfrlem9  8421  oe0lem  8549  oa00  8595  omwordi  8607  om00  8611  omass  8616  oelim2  8632  oeoa  8634  oeoe  8636  nnmwordi  8672  swoso  8780  dom2lem  9047  onsdominel  9173  f1finf1o  9292  fiint  9346  cantnfp1lem3  9708  cantnfp1  9709  cantnflem1  9717  ttrclselem2  9754  rankr1ai  9833  rankval3b  9863  harcard  10086  infxpenlem  10119  alephnbtwn  10177  alephinit  10201  infxp  10319  cofsmo  10374  infpssALT  10418  fin23lem24  10427  fin56  10498  ttukeylem6  10619  ficard  10676  alephval2  10684  fpwwe2lem7  10749  fpwwe2  10755  gchdju1  10768  pwfseqlem3  10772  pwfseqlem4a  10773  pwfseqlem4  10774  gchpwdom  10782  tskss  10870  inar1  10887  gruss  10908  gruurn  10910  ltsonq  11081  distrlem4pr  11138  sqgt0sr  11218  map2psrpr  11222  letric  11437  renegcli  11646  addid0  11762  mulge0b  12214  nnge1  12393  0mnnnnn0  12665  nn0lt2  12789  zneo  12809  uzind2  12819  fzind  12824  nn0ind-raph  12826  uzwo  13065  nn01to3  13095  zbtwnre  13100  rpnnen1lem5  13136  ledivge1le  13220  xrletri  13309  qsqueeze  13358  difreicc  13642  elfzmlbp  13800  difelfznle  13803  elfzodifsumelfzo  13893  ssfzo12  13921  elfzonelfzo  13931  flflp1  13974  fleqceilz  14021  modsumfzodifsn  14114  addmodlteq  14116  om2uzf1oi  14123  expnngt1  14412  facdiv  14458  facwordi  14460  bcpasc  14492  hashdom  14550  hashgt23el  14596  hashdmpropge2  14655  ccatsymb  14755  swrdnnn0nd  14834  swrdnd0  14835  swrdsbslen  14842  swrdspsleq  14843  swrdlsw  14845  pfxnd0  14866  swrdswrdlem  14881  swrdccatin1  14902  pfxccatin12lem3  14909  swrdccat  14912  pfxccat3a  14915  repswswrd  14963  cshwidx0  14985  cshwcsh2id  15007  limsupbnd1  15678  lo1bdd2  15720  addcn2  15790  mulcn2  15792  o1rlimmul  15815  lo1add  15823  lo1mul  15824  rlimno1  15850  ruclem3  16430  odd2np1  16540  oddge22np1  16548  bitsfzo  16634  cncongr1  16871  2mulprm  16897  prm23ge5  17022  pcdvdsb  17076  pcaddlem  17095  infpnlem1  17117  prmunb  17121  vdwlem9  17196  vdwnnlem3  17204  ramcl  17236  prmgaplem5  17262  cshwshash  17311  setcmon  18291  setcepi  18292  setciso  18295  xpsmnd0  19001  f1ghm0to0  19488  ghmf1  19489  imasgim  19513  sylow2alem2  19862  sylow2blem3  19866  qusabl  20109  lt6abl  20139  cyggexb  20143  gsumcom2  20219  ringurd  20441  imasring  20590  xpsring1d  20593  0ring1eq0  20815  subrgdvds  20868  rngciso  20920  ringciso  20954  isdomn4  20997  drnginvrcl  21041  drnginvrl  21044  drnginvrr  21045  lsmelval2  21390  quscrng  21609  xrsdsreclblem  21749  obs2ss  22065  obslbs  22066  rnasclassa  22233  mplsubrglem  22341  psdmul  22517  gsummoncoe1  22656  mp2pm2mplem4  23157  chfacfisf  23202  chfacfisfcpmat  23203  cayleyhamilton1  23240  cmpsublem  23747  cmpsub  23748  1stccnp  23811  locfincf  23880  txhaus  23996  xkohaus  24002  ufilss  24254  cfinufil  24277  fmfnfmlem1  24303  hausflim  24330  fclscf  24374  alexsubb  24395  qustgplem  24470  prdsbl  24840  metss2lem  24860  nghmcn  25094  cfil3i  25620  cmetcaulem  25639  minveclem4  25783  ovolgelb  25831  ovolunnul  25851  ovoliun  25856  ovoliunnul  25858  ovolicc2lem2  25869  iundisj2  25900  voliunlem3  25903  rolle  26340  dvlip  26343  lhop1lem  26363  lhop2  26365  dvfsumrlim  26381  deg1ge  26446  coeeulem  26573  dgrco  26624  radcnvlt1  26775  psercnlem1  26782  logcnlem2  27001  logcnlem3  27002  cxpeq  27115  angpined  27188  efrlim  27327  dmgmaddn0  27380  lgamucov  27395  basellem2  27439  ppieq0  27533  mumullem2  27537  chpeq0  27565  chteq0  27566  chtub  27569  fsumvma  27570  dchrptlem1  27621  bposlem6  27646  gausslemma2dlem0i  27721  gausslemma2dlem1a  27722  lgseisenlem2  27733  2sqlem6  27780  2sq2  27790  2sqnn0  27795  2sqreulem1  27803  2sqreunnlem1  27806  dchrisum0lem1  27873  pntrsumbnd2  27924  pntlem3  27966  fltoprmlem2  28024  noextenddif  28055  nosupno  28090  nosupbnd1  28101  noinfno  28105  noinfbnd1  28116  noetasuplem4  28123  noetainflem4  28127  cutsun12  28206  lesrec  28215  cutlt  28348  leadds2im  28404  oniso  28687  n0fincut  28771  bdayfinbndlem1  28883  z12bdaylem1  28886  colinearalg  29518  eengtrkg  29594  incistruhgr  29687  wlkv0  30260  crctcshwlkn0  30440  clwwlkccatlem  30610  clwlkclwwlklem2a4  30618  clwlkclwwlklem2  30621  clwlkclwwlkfo  30630  eucrctshift  30874  frrusgrord0  30971  frgrreg  31025  blocni  31437  ubthlem1  31502  minvecolem4  31512  shmodsi  32021  atcvati  33018  atcvat2i  33019  chirredlem4  33025  atmd2  33032  sumdmdlem  33050  addltmulALT  33120  iundisj2f  33256  iundisj2fi  33459  erdszelem9  36131  satffunlem1lem2  36335  satffunlem2lem2  36338  rdgprc  36734  cgrsub  36988  btwnxfr  36999  lineext  37019  linecgr  37024  btwnconn1lem4  37033  btwnconn1lem5  37034  btwnconn1lem6  37035  btwnconn1lem8  37037  btwnconn1lem11  37040  mptsnunlem  38453  finxpreclem6  38511  ltflcei  38723  poimirlem23  38753  poimirlem24  38754  poimirlem31  38761  poimirlem32  38762  ftc1anclem5  38807  heiborlem6  38942  grpokerinj  39019  dvrunz  39080  isdmn3  39200  dmncan1  39202  membpartlem19  40038  l1cvpat  40303  atnle  40566  cvlexch3  40581  cvlexch4N  40582  cvlatexchb1  40583  cvrat2  40678  atlelt  40687  3dimlem4a  40712  3dimlem4OLDN  40714  ps-1  40726  ps-2  40727  4atlem10  40855  4atlem11  40858  4atlem12  40861  cdleme11c  41510  cdleme21c  41576  cdlemg6d  41870  trlcoat  41972  tendoid0  42074  cdleml3N  42227  dia2dimlem7  42319  aks6d1c6lem3  43414  expeq1d  43574  fsuppind  43811  pellexlem1  44029  pellexlem6  44034  onsupmaxb  44433  safesnsupfidom1o  44610  reabsifnpos  44825  reabsifnneg  44827  iunrelexpmin1  44900  iunrelexpmin2  44904  radcnvrat  45490  nzss  45493  pwclaxpow  46169  ormkglobd  48092  elprneb  48304  or2expropbi  48309  tz6.12i-afv2  48518  dfatcolem  48530  f1oresf1o2  48566  zm1nn  48577  2ffzoeq  48603  modmkpkne  48642  sfprmdvdsmersenne  48893  lighneallem3  48897  lighneallem4  48900  requad01  48924  fppr2odd  49034  fpprwppr  49042  stgoldbwt  49079  sbgoldbaltlem1  49082  isuspgrimlem  49198  upgrimpthslem2  49211  isubgr3stgrlem4  49272  isubgr3stgrlem7  49275  gpg5nbgrvtx03starlem1  49371  gpg5nbgrvtx03starlem3  49373  gpg5nbgrvtx13starlem1  49374  gpg5nbgrvtx13starlem3  49376  lmod0rng  49531  lidldomn1  49533  rngcisoALTV  49579  ringcisoALTV  49613  isidom3  49647  idomcanl  49649  ztprmneprm  49664  lincresunit3  49798  itsclc0yqsol  50081  itschlc0xyqsol1  50083  aacllem  51219