Theorem sylbird 259

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

Syntax hints:   → wi 4   ↔ wb 205

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 206

This theorem is referenced by:  3imtr3d  292  ceqex  3639  eqreu  3724  sotr2  5619  sotr3  5626  sossfld  6182  ordintdif  6411  tz6.12i  6916  f1cofveqaeqALT  7254  soisoi  7321  riotaeqimp  7388  ov3  7566  tfindsg  7846  tfindsg2  7847  nnsuc  7869  findsg  7886  soseq  8141  suppssr  8177  suppssrg  8178  tfrlem9  8381  oe0lem  8509  oa00  8555  omwordi  8567  om00  8571  omass  8576  oelim2  8591  oeoa  8593  oeoe  8595  nnmwordi  8631  swoso  8732  dom2lem  8984  onsdominel  9122  f1finf1o  9267  f1finf1oOLD  9268  cantnfp1lem3  9671  cantnfp1  9672  cantnflem1  9680  ttrclselem2  9717  rankr1ai  9789  rankval3b  9817  harcard  9969  infxpenlem  10004  alephnbtwn  10062  alephinit  10086  infxp  10206  cofsmo  10260  infpssALT  10304  fin23lem24  10313  fin56  10384  ttukeylem6  10505  ficard  10556  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  11310  renegcli  11517  addid0  11629  mulge0b  12080  nnge1  12236  0mnnnnn0  12500  nn0lt2  12621  zneo  12641  uzind2  12651  fzind  12656  nn0ind-raph  12658  uzwo  12891  nn01to3  12921  zbtwnre  12926  rpnnen1lem5  12961  ledivge1le  13041  xrletri  13128  qsqueeze  13176  difreicc  13457  elfzmlbp  13608  difelfznle  13611  elfzodifsumelfzo  13694  ssfzo12  13721  elfzonelfzo  13730  flflp1  13768  fleqceilz  13815  modsumfzodifsn  13905  addmodlteq  13907  om2uzf1oi  13914  expnngt1  14200  facdiv  14243  facwordi  14245  bcpasc  14277  hashdom  14335  hashgt23el  14380  hashdmpropge2  14440  ccatsymb  14528  swrdnnn0nd  14602  swrdnd0  14603  swrdsbslen  14610  swrdspsleq  14611  swrdlsw  14613  pfxnd0  14634  swrdswrdlem  14650  swrdccatin1  14671  pfxccatin12lem3  14678  swrdccat  14681  pfxccat3a  14684  repswswrd  14730  cshwidx0  14752  cshwcsh2id  14775  limsupbnd1  15422  lo1bdd2  15464  addcn2  15534  mulcn2  15536  o1rlimmul  15559  lo1add  15567  lo1mul  15568  rlimno1  15596  ruclem3  16172  odd2np1  16280  oddge22np1  16288  bitsfzo  16372  cncongr1  16600  2mulprm  16626  prm23ge5  16744  pcdvdsb  16798  pcaddlem  16817  infpnlem1  16839  prmunb  16843  vdwlem9  16918  vdwnnlem3  16926  ramcl  16958  prmgaplem5  16984  cshwshash  17034  setcmon  18033  setcepi  18034  setciso  18037  xpsmnd0  18662  ghmf1  19115  sylow2alem2  19480  sylow2blem3  19484  qusabl  19727  lt6abl  19757  cyggexb  19761  gsumcom2  19837  imasring  20136  f1ghm0to0  20271  drnginvrcl  20329  drnginvrl  20332  drnginvrr  20333  subrgdvds  20369  lsmelval2  20688  quscrng  20870  isdomn4  20910  xrsdsreclblem  20983  obs2ss  21275  obslbs  21276  rnasclassa  21440  mplsubrglem  21554  gsummoncoe1  21819  mp2pm2mplem4  22302  chfacfisf  22347  chfacfisfcpmat  22348  cayleyhamilton1  22385  cmpsublem  22894  cmpsub  22895  1stccnp  22957  locfincf  23026  txhaus  23142  xkohaus  23148  ufilss  23400  cfinufil  23423  fmfnfmlem1  23449  hausflim  23476  fclscf  23520  alexsubb  23541  qustgplem  23616  prdsbl  23991  metss2lem  24011  nghmcn  24253  cfil3i  24777  cmetcaulem  24796  minveclem4  24940  ovolgelb  24988  ovolunnul  25008  ovoliun  25013  ovoliunnul  25015  ovolicc2lem2  25026  iundisj2  25057  voliunlem3  25060  rolle  25498  dvlip  25501  lhop1lem  25521  lhop2  25523  dvfsumrlim  25539  deg1ge  25607  coeeulem  25729  dgrco  25780  radcnvlt1  25921  psercnlem1  25928  logcnlem2  26142  logcnlem3  26143  cxpeq  26254  angpined  26324  efrlim  26463  dmgmaddn0  26516  lgamucov  26531  basellem2  26575  ppieq0  26669  mumullem2  26673  chpeq0  26700  chteq0  26701  chtub  26704  fsumvma  26705  dchrptlem1  26756  bposlem6  26781  gausslemma2dlem0i  26856  gausslemma2dlem1a  26857  lgseisenlem2  26868  2sqlem6  26915  2sq2  26925  2sqnn0  26930  2sqreulem1  26938  2sqreunnlem1  26941  dchrisum0lem1  27008  pntrsumbnd2  27059  pntlem3  27101  noextenddif  27160  nosupno  27195  nosupbnd1  27206  noinfno  27210  noinfbnd1  27221  noetasuplem4  27228  noetainflem4  27232  scutun12  27300  slerec  27309  cutlt  27408  sleadd2im  27460  colinearalg  28157  eengtrkg  28233  incistruhgr  28328  wlkv0  28897  crctcshwlkn0  29064  clwwlkccatlem  29231  clwlkclwwlklem2a4  29239  clwlkclwwlklem2  29242  clwlkclwwlkfo  29251  eucrctshift  29485  frrusgrord0  29582  frgrreg  29636  blocni  30045  ubthlem1  30110  minvecolem4  30120  shmodsi  30629  atcvati  31626  atcvat2i  31627  chirredlem4  31633  atmd2  31640  sumdmdlem  31658  addltmulALT  31686  iundisj2f  31808  iundisj2fi  31995  rngurd  32367  f1resveqaeq  34076  erdszelem9  34178  satffunlem1lem2  34382  satffunlem2lem2  34385  rdgprc  34754  cgrsub  35005  btwnxfr  35016  lineext  35036  linecgr  35041  btwnconn1lem4  35050  btwnconn1lem5  35051  btwnconn1lem6  35052  btwnconn1lem8  35054  btwnconn1lem11  35057  mptsnunlem  36207  finxpreclem6  36265  ltflcei  36464  poimirlem23  36499  poimirlem24  36500  poimirlem31  36507  poimirlem32  36508  ftc1anclem5  36553  heiborlem6  36672  grpokerinj  36749  dvrunz  36810  isdmn3  36930  dmncan1  36932  membpartlem19  37669  l1cvpat  37912  atnle  38175  cvlexch3  38190  cvlexch4N  38191  cvlatexchb1  38192  cvrat2  38288  atlelt  38297  3dimlem4a  38322  3dimlem4OLDN  38324  ps-1  38336  ps-2  38337  4atlem10  38465  4atlem11  38468  4atlem12  38471  cdleme11c  39120  cdleme21c  39186  cdlemg6d  39480  trlcoat  39582  tendoid0  39684  cdleml3N  39837  dia2dimlem7  39929  metakunt1  40973  metakunt6  40978  fsuppind  41159  pellexlem1  41552  pellexlem6  41557  imasgim  41827  onsupmaxb  41973  safesnsupfidom1o  42153  reabsifnpos  42369  reabsifnneg  42371  iunrelexpmin1  42444  iunrelexpmin2  42448  radcnvrat  43058  nzss  43061  elprneb  45725  or2expropbi  45730  tz6.12i-afv2  45937  dfatcolem  45949  f1oresf1o2  45985  zm1nn  45996  2ffzoeq  46022  sfprmdvdsmersenne  46257  lighneallem3  46261  lighneallem4  46264  requad01  46275  fppr2odd  46385  fpprwppr  46393  stgoldbwt  46430  sbgoldbaltlem1  46433  isomuspgrlem1  46481  lmod0rng  46628  0ring1eq0  46632  lidldomn1  46776  rngciso  46833  rngcisoALTV  46845  ringciso  46884  ringcisoALTV  46908  ztprmneprm  46976  lincresunit3  47115  itsclc0yqsol  47403  itschlc0xyqsol1  47405  aacllem  47801