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  5592  sotr3  5599  sossfld  6177  ordintdif  6414  tz6.12i  6911  f1cofveqaeqALT  7262  f1resveqaeq  7277  soisoi  7336  riotaeqimp  7403  ov3  7583  tfindsg  7872  tfindsg2  7873  nnsuc  7895  findsg  7909  soseq  8176  suppssr  8213  suppssrg  8214  tfrlem9  8394  oe0lem  8522  oa00  8568  omwordi  8580  om00  8584  omass  8589  oelim2  8605  oeoa  8607  oeoe  8609  nnmwordi  8645  swoso  8753  dom2lem  9020  onsdominel  9146  f1finf1o  9265  fiint  9319  cantnfp1lem3  9682  cantnfp1  9683  cantnflem1  9691  ttrclselem2  9728  rankr1ai  9807  rankval3b  9837  harcard  10060  infxpenlem  10093  alephnbtwn  10151  alephinit  10175  infxp  10293  cofsmo  10348  infpssALT  10392  fin23lem24  10401  fin56  10472  ttukeylem6  10593  ficard  10650  alephval2  10658  fpwwe2lem7  10723  fpwwe2  10729  gchdju1  10742  pwfseqlem3  10746  pwfseqlem4a  10747  pwfseqlem4  10748  gchpwdom  10756  tskss  10844  inar1  10861  gruss  10882  gruurn  10884  ltsonq  11055  distrlem4pr  11112  sqgt0sr  11192  map2psrpr  11196  letric  11411  renegcli  11620  addid0  11736  mulge0b  12188  nnge1  12367  0mnnnnn0  12639  nn0lt2  12763  zneo  12783  uzind2  12793  fzind  12798  nn0ind-raph  12800  uzwo  13039  nn01to3  13069  zbtwnre  13074  rpnnen1lem5  13110  ledivge1le  13194  xrletri  13283  qsqueeze  13332  difreicc  13616  elfzmlbp  13774  difelfznle  13777  elfzodifsumelfzo  13867  ssfzo12  13895  elfzonelfzo  13905  flflp1  13948  fleqceilz  13995  modsumfzodifsn  14088  addmodlteq  14090  om2uzf1oi  14097  expnngt1  14386  facdiv  14432  facwordi  14434  bcpasc  14466  hashdom  14524  hashgt23el  14570  hashdmpropge2  14629  ccatsymb  14729  swrdnnn0nd  14807  swrdnd0  14808  swrdsbslen  14815  swrdspsleq  14816  swrdlsw  14818  pfxnd0  14839  swrdswrdlem  14854  swrdccatin1  14875  pfxccatin12lem3  14882  swrdccat  14885  pfxccat3a  14888  repswswrd  14936  cshwidx0  14958  cshwcsh2id  14980  limsupbnd1  15650  lo1bdd2  15692  addcn2  15762  mulcn2  15764  o1rlimmul  15787  lo1add  15795  lo1mul  15796  rlimno1  15822  ruclem3  16402  odd2np1  16512  oddge22np1  16520  bitsfzo  16606  cncongr1  16843  2mulprm  16869  prm23ge5  16994  pcdvdsb  17048  pcaddlem  17067  infpnlem1  17089  prmunb  17093  vdwlem9  17168  vdwnnlem3  17176  ramcl  17208  prmgaplem5  17234  cshwshash  17283  setcmon  18263  setcepi  18264  setciso  18267  xpsmnd0  18973  f1ghm0to0  19460  ghmf1  19461  sylow2alem2  19833  sylow2blem3  19837  qusabl  20080  lt6abl  20110  cyggexb  20114  gsumcom2  20190  ringurd  20412  imasring  20561  xpsring1d  20564  0ring1eq0  20786  subrgdvds  20839  rngciso  20891  ringciso  20925  isdomn4  20968  drnginvrcl  21012  drnginvrl  21015  drnginvrr  21016  lsmelval2  21361  quscrng  21580  xrsdsreclblem  21720  obs2ss  22036  obslbs  22037  rnasclassa  22204  mplsubrglem  22312  psdmul  22488  gsummoncoe1  22627  mp2pm2mplem4  23128  chfacfisf  23173  chfacfisfcpmat  23174  cayleyhamilton1  23211  cmpsublem  23718  cmpsub  23719  1stccnp  23782  locfincf  23851  txhaus  23967  xkohaus  23973  ufilss  24225  cfinufil  24248  fmfnfmlem1  24274  hausflim  24301  fclscf  24345  alexsubb  24366  qustgplem  24441  prdsbl  24811  metss2lem  24831  nghmcn  25065  cfil3i  25591  cmetcaulem  25610  minveclem4  25754  ovolgelb  25802  ovolunnul  25822  ovoliun  25827  ovoliunnul  25829  ovolicc2lem2  25840  iundisj2  25871  voliunlem3  25874  rolle  26311  dvlip  26314  lhop1lem  26334  lhop2  26336  dvfsumrlim  26352  deg1ge  26417  coeeulem  26544  dgrco  26595  radcnvlt1  26746  psercnlem1  26753  logcnlem2  26972  logcnlem3  26973  cxpeq  27086  angpined  27159  efrlim  27298  dmgmaddn0  27351  lgamucov  27366  basellem2  27410  ppieq0  27504  mumullem2  27508  chpeq0  27536  chteq0  27537  chtub  27540  fsumvma  27541  dchrptlem1  27592  bposlem6  27617  gausslemma2dlem0i  27692  gausslemma2dlem1a  27693  lgseisenlem2  27704  2sqlem6  27751  2sq2  27761  2sqnn0  27766  2sqreulem1  27774  2sqreunnlem1  27777  dchrisum0lem1  27844  pntrsumbnd2  27895  pntlem3  27937  fltoprmlem2  27995  noextenddif  28026  nosupno  28061  nosupbnd1  28072  noinfno  28076  noinfbnd1  28087  noetasuplem4  28094  noetainflem4  28098  cutsun12  28177  lesrec  28186  cutlt  28319  leadds2im  28375  oniso  28658  n0fincut  28742  bdayfinbndlem1  28854  z12bdaylem1  28857  colinearalg  29489  eengtrkg  29565  incistruhgr  29658  wlkv0  30231  crctcshwlkn0  30411  clwwlkccatlem  30581  clwlkclwwlklem2a4  30589  clwlkclwwlklem2  30592  clwlkclwwlkfo  30601  eucrctshift  30845  frrusgrord0  30942  frgrreg  30996  blocni  31408  ubthlem1  31473  minvecolem4  31483  shmodsi  31992  atcvati  32989  atcvat2i  32990  chirredlem4  32996  atmd2  33003  sumdmdlem  33021  addltmulALT  33091  iundisj2f  33227  iundisj2fi  33432  erdszelem9  36033  satffunlem1lem2  36237  satffunlem2lem2  36240  rdgprc  36631  cgrsub  36885  btwnxfr  36896  lineext  36916  linecgr  36921  btwnconn1lem4  36930  btwnconn1lem5  36931  btwnconn1lem6  36932  btwnconn1lem8  36934  btwnconn1lem11  36937  mptsnunlem  38337  finxpreclem6  38395  ltflcei  38607  poimirlem23  38637  poimirlem24  38638  poimirlem31  38645  poimirlem32  38646  ftc1anclem5  38691  heiborlem6  38826  grpokerinj  38903  dvrunz  38964  isdmn3  39084  dmncan1  39086  membpartlem19  39922  l1cvpat  40187  atnle  40450  cvlexch3  40465  cvlexch4N  40466  cvlatexchb1  40467  cvrat2  40562  atlelt  40571  3dimlem4a  40596  3dimlem4OLDN  40598  ps-1  40610  ps-2  40611  4atlem10  40739  4atlem11  40742  4atlem12  40745  cdleme11c  41394  cdleme21c  41460  cdlemg6d  41754  trlcoat  41856  tendoid0  41958  cdleml3N  42111  dia2dimlem7  42203  aks6d1c6lem3  43298  expeq1d  43457  fsuppind  43694  pellexlem1  43912  pellexlem6  43917  imasgim  44178  onsupmaxb  44317  safesnsupfidom1o  44494  reabsifnpos  44709  reabsifnneg  44711  iunrelexpmin1  44784  iunrelexpmin2  44788  radcnvrat  45374  nzss  45377  pwclaxpow  46050  ormkglobd  47963  elprneb  48175  or2expropbi  48180  tz6.12i-afv2  48389  dfatcolem  48401  f1oresf1o2  48437  zm1nn  48448  2ffzoeq  48474  modmkpkne  48513  sfprmdvdsmersenne  48764  lighneallem3  48768  lighneallem4  48771  requad01  48795  fppr2odd  48905  fpprwppr  48913  stgoldbwt  48950  sbgoldbaltlem1  48953  isuspgrimlem  49069  upgrimpthslem2  49082  isubgr3stgrlem4  49143  isubgr3stgrlem7  49146  gpg5nbgrvtx03starlem1  49242  gpg5nbgrvtx03starlem3  49244  gpg5nbgrvtx13starlem1  49245  gpg5nbgrvtx13starlem3  49247  lmod0rng  49402  lidldomn1  49404  rngcisoALTV  49450  ringcisoALTV  49484  isidom3  49518  idomcanl  49520  ztprmneprm  49535  lincresunit3  49669  itsclc0yqsol  49952  itschlc0xyqsol1  49954  aacllem  51015