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 ⊢ (𝜑 → (𝜓 → 𝜃))

Syntax hints:   → wi 4   ↔ wb 209

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 210

This theorem is referenced by:  3imtr3d  296  ceqex  3610  eqreu  3691  sotr2  5603  sotr3  5610  sossfld  6184  ordintdif  6412  tz6.12i  6907  f1cofveqaeqALT  7256  soisoi  7326  riotaeqimp  7393  ov3  7573  tfindsg  7856  tfindsg2  7857  nnsuc  7879  findsg  7893  soseq  8154  suppssr  8190  suppssrg  8191  tfrlem9  8371  oe0lem  8497  oa00  8543  omwordi  8555  om00  8559  omass  8564  oelim2  8580  oeoa  8582  oeoe  8584  nnmwordi  8620  swoso  8728  dom2lem  8988  onsdominel  9113  f1finf1o  9232  fiint  9285  cantnfp1lem3  9648  cantnfp1  9649  cantnflem1  9657  ttrclselem2  9694  rankr1ai  9769  rankval3b  9797  harcard  9963  infxpenlem  9996  alephnbtwn  10054  alephinit  10078  infxp  10196  cofsmo  10252  infpssALT  10296  fin23lem24  10305  fin56  10376  ttukeylem6  10497  ficard  10548  alephval2  10556  fpwwe2lem7  10621  fpwwe2  10627  gchdju1  10640  pwfseqlem3  10644  pwfseqlem4a  10645  pwfseqlem4  10646  gchpwdom  10654  tskss  10742  inar1  10759  gruss  10780  gruurn  10782  ltsonq  10953  distrlem4pr  11010  sqgt0sr  11090  map2psrpr  11094  letric  11309  renegcli  11518  addid0  11632  mulge0b  12084  nnge1  12263  0mnnnnn0  12535  nn0lt2  12658  zneo  12678  uzind2  12688  fzind  12693  nn0ind-raph  12695  uzwo  12934  nn01to3  12964  zbtwnre  12969  rpnnen1lem5  13004  ledivge1le  13088  xrletri  13177  qsqueeze  13226  difreicc  13510  elfzmlbp  13667  difelfznle  13670  elfzodifsumelfzo  13760  ssfzo12  13788  elfzonelfzo  13798  flflp1  13840  fleqceilz  13887  modsumfzodifsn  13980  addmodlteq  13982  om2uzf1oi  13989  expnngt1  14277  facdiv  14323  facwordi  14325  bcpasc  14357  hashdom  14415  hashgt23el  14461  hashdmpropge2  14520  ccatsymb  14620  swrdnnn0nd  14694  swrdnd0  14695  swrdsbslen  14702  swrdspsleq  14703  swrdlsw  14705  pfxnd0  14726  swrdswrdlem  14741  swrdccatin1  14762  pfxccatin12lem3  14769  swrdccat  14772  pfxccat3a  14775  repswswrd  14821  cshwidx0  14843  cshwcsh2id  14865  limsupbnd1  15533  lo1bdd2  15575  addcn2  15645  mulcn2  15647  o1rlimmul  15670  lo1add  15678  lo1mul  15679  rlimno1  15705  ruclem3  16288  odd2np1  16398  oddge22np1  16406  bitsfzo  16492  cncongr1  16724  2mulprm  16750  prm23ge5  16874  pcdvdsb  16928  pcaddlem  16947  infpnlem1  16969  prmunb  16973  vdwlem9  17048  vdwnnlem3  17056  ramcl  17088  prmgaplem5  17114  cshwshash  17163  setcmon  18143  setcepi  18144  setciso  18147  xpsmnd0  18835  f1ghm0to0  19314  ghmf1  19315  sylow2alem2  19687  sylow2blem3  19691  qusabl  19934  lt6abl  19964  cyggexb  19968  gsumcom2  20044  ringurd  20266  imasring  20411  xpsring1d  20414  0ring1eq0  20617  subrgdvds  20670  rngciso  20722  ringciso  20756  isdomn4  20799  drnginvrcl  20837  drnginvrl  20840  drnginvrr  20841  lsmelval2  21185  quscrng  21402  xrsdsreclblem  21542  obs2ss  21858  obslbs  21859  rnasclassa  22024  mplsubrglem  22132  psdmul  22308  gsummoncoe1  22447  mp2pm2mplem4  22945  chfacfisf  22990  chfacfisfcpmat  22991  cayleyhamilton1  23028  cmpsublem  23535  cmpsub  23536  1stccnp  23598  locfincf  23667  txhaus  23783  xkohaus  23789  ufilss  24041  cfinufil  24064  fmfnfmlem1  24090  hausflim  24117  fclscf  24161  alexsubb  24182  qustgplem  24257  prdsbl  24627  metss2lem  24647  nghmcn  24881  cfil3i  25407  cmetcaulem  25426  minveclem4  25570  ovolgelb  25618  ovolunnul  25638  ovoliun  25643  ovoliunnul  25645  ovolicc2lem2  25656  iundisj2  25687  voliunlem3  25690  rolle  26128  dvlip  26131  lhop1lem  26151  lhop2  26153  dvfsumrlim  26169  deg1ge  26234  coeeulem  26360  dgrco  26411  radcnvlt1  26557  psercnlem1  26564  logcnlem2  26784  logcnlem3  26785  cxpeq  26898  angpined  26971  efrlim  27110  dmgmaddn0  27163  lgamucov  27178  basellem2  27222  ppieq0  27316  mumullem2  27320  chpeq0  27348  chteq0  27349  chtub  27352  fsumvma  27353  dchrptlem1  27404  bposlem6  27429  gausslemma2dlem0i  27504  gausslemma2dlem1a  27505  lgseisenlem2  27516  2sqlem6  27563  2sq2  27573  2sqnn0  27578  2sqreulem1  27586  2sqreunnlem1  27589  dchrisum0lem1  27656  pntrsumbnd2  27707  pntlem3  27749  noextenddif  27808  nosupno  27843  nosupbnd1  27854  noinfno  27858  noinfbnd1  27869  noetasuplem4  27876  noetainflem4  27880  cutsun12  27959  lesrec  27968  cutlt  28101  leadds2im  28157  oniso  28440  n0fincut  28524  bdayfinbndlem1  28636  z12bdaylem1  28639  colinearalg  29226  eengtrkg  29302  incistruhgr  29395  wlkv0  29965  crctcshwlkn0  30136  clwwlkccatlem  30306  clwlkclwwlklem2a4  30314  clwlkclwwlklem2  30317  clwlkclwwlkfo  30326  eucrctshift  30560  frrusgrord0  30657  frgrreg  30711  blocni  31123  ubthlem1  31188  minvecolem4  31198  shmodsi  31707  atcvati  32704  atcvat2i  32705  chirredlem4  32711  atmd2  32718  sumdmdlem  32736  addltmulALT  32764  iundisj2f  32901  iundisj2fi  33108  f1resveqaeq  35439  erdszelem9  35657  satffunlem1lem2  35861  satffunlem2lem2  35864  rdgprc  36250  cgrsub  36503  btwnxfr  36514  lineext  36534  linecgr  36539  btwnconn1lem4  36548  btwnconn1lem5  36549  btwnconn1lem6  36550  btwnconn1lem8  36552  btwnconn1lem11  36555  mh-inf3f1  37018  mptsnunlem  37950  finxpreclem6  38008  ltflcei  38225  poimirlem23  38260  poimirlem24  38261  poimirlem31  38268  poimirlem32  38269  ftc1anclem5  38314  heiborlem6  38433  grpokerinj  38510  dvrunz  38571  isdmn3  38691  dmncan1  38693  membpartlem19  39531  l1cvpat  39796  atnle  40059  cvlexch3  40074  cvlexch4N  40075  cvlatexchb1  40076  cvrat2  40171  atlelt  40180  3dimlem4a  40205  3dimlem4OLDN  40207  ps-1  40219  ps-2  40220  4atlem10  40348  4atlem11  40351  4atlem12  40354  cdleme11c  41003  cdleme21c  41069  cdlemg6d  41363  trlcoat  41465  tendoid0  41567  cdleml3N  41720  dia2dimlem7  41812  aks6d1c6lem3  42907  expeq1d  43053  fsuppind  43292  pellexlem1  43526  pellexlem6  43531  imasgim  43797  onsupmaxb  43936  safesnsupfidom1o  44113  reabsifnpos  44329  reabsifnneg  44331  iunrelexpmin1  44404  iunrelexpmin2  44408  radcnvrat  44994  nzss  44997  pwclaxpow  45663  ormkglobd  47561  elprneb  47733  or2expropbi  47738  tz6.12i-afv2  47947  dfatcolem  47959  f1oresf1o2  47995  zm1nn  48006  2ffzoeq  48032  modmkpkne  48071  sfprmdvdsmersenne  48322  lighneallem3  48326  lighneallem4  48329  requad01  48353  fppr2odd  48463  fpprwppr  48471  stgoldbwt  48508  sbgoldbaltlem1  48511  isuspgrimlem  48627  upgrimpthslem2  48640  isubgr3stgrlem4  48701  isubgr3stgrlem7  48704  gpg5nbgrvtx03starlem1  48800  gpg5nbgrvtx03starlem3  48802  gpg5nbgrvtx13starlem1  48803  gpg5nbgrvtx13starlem3  48805  lmod0rng  48961  lidldomn1  48963  rngcisoALTV  49009  ringcisoALTV  49043  isidom3  49077  idomcanl  49079  ztprmneprm  49094  lincresunit3  49228  itsclc0yqsol  49511  itschlc0xyqsol1  49513  aacllem  50568