Theorem sylan2br 594

Description: A syllogism inference. (Contributed by NM, 21-Apr-1994.)

Hypotheses

Ref	Expression
sylan2br.1	⊢ (𝜒 ↔ 𝜑)
sylan2br.2	⊢ ((𝜓 ∧ 𝜒) → 𝜃)

Assertion

Ref	Expression
sylan2br	⊢ ((𝜓 ∧ 𝜑) → 𝜃)

Proof of Theorem sylan2br

Step	Hyp	Ref	Expression
1		sylan2br.1	. . 3 ⊢ (𝜒 ↔ 𝜑)
2	1	biimpri 227	. 2 ⊢ (𝜑 → 𝜒)
3		sylan2br.2	. 2 ⊢ ((𝜓 ∧ 𝜒) → 𝜃)
4	2, 3	sylan2 592	1 ⊢ ((𝜓 ∧ 𝜑) → 𝜃)

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 395

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  df-an 396

This theorem is referenced by:  syl2anbr  598  pm2.61danel  3062  imainss  6046  funeu2  6444  imadif  6502  fnop  6526  ssimaex  6835  tfindsg2  7683  nn0suc  7716  xpexr2  7740  extmptsuppeq  7975  suppss  7981  suppssOLD  7982  suppss2  7987  frrlem14  8086  wfr3g  8109  smores3  8155  tfr3ALT  8204  tz7.48-2  8243  swoso  8489  entrfil  8931  domtrfi  8938  isinf  8965  frfi  8989  dffi3  9120  marypha1lem  9122  ordtypelem7  9213  cnfcom2lem  9389  r1pw  9534  rankxplim3  9570  dfac5  9815  cofsmo  9956  axcclem  10144  zorn2lem7  10189  wloglei  11437  divval  11565  uzind3  12344  xrltnsym  12800  xaddf  12887  xrsupsslem  12970  xrinfmsslem  12971  0fz1  13205  hashunsng  14035  hashunsngx  14036  hashgt0elexb  14045  sumss  15364  fsumss  15365  fsumcvg3  15369  abscvgcvg  15459  isumshft  15479  geoisum1  15519  geoisum1c  15520  mertenslem2  15525  zprod  15575  prodss  15585  fprodss  15586  rpnnen2lem5  15855  gcdcllem3  16136  lcmgcd  16240  lcmdvds  16241  lcmfval  16254  lcmfcl  16261  dvdslcmf  16264  isprm2lem  16314  eulerthlem2  16411  ramcl2lem  16638  imasvscafn  17165  mreexexlem4d  17273  cycsubgcl  18740  galactghm  18927  odlem2  19062  gexlem2  19102  mulgmhm  19344  mulgghm  19345  gsumval3  19423  gsumpt  19478  dprdfeq0  19540  srglmhm  19686  srgrmhm  19687  ringlghm  19758  ringrghm  19759  sdrgacs  19984  cntzsdrg  19985  lssssr  20130  lbsind  20257  cnsubrg  20570  mplmonmul  21147  mplcoe1  21148  mplcoe5  21151  matplusgcell  21490  elcls  22132  neips  22172  opnnei  22179  ordtbaslem  22247  ptclsg  22674  qtopeu  22775  xmetpsmet  23409  comet  23575  metrest  23586  pcorevlem  24095  dyadmbl  24669  mbfeqalem1  24710  i1fadd  24764  itg1addlem2  24766  itg2uba  24813  itgss  24881  dvcnp  24988  quotval  25357  vieta1lem2  25376  aalioulem3  25399  ulmdvlem3  25466  dvradcnv  25485  abelthlem6  25500  abelthlem9  25504  abelth  25505  logtayllem  25719  logtayl  25720  cxpcl  25734  recxpcl  25735  cxpcn3lem  25805  leibpi  25997  musum  26245  dchrelbas3  26291  sumdchr2  26323  lgscllem  26357  lgsdir2  26383  dchrvmasumiflem2  26555  rpvmasum2  26565  padicabv  26683  padicabvf  26684  padicabvcxp  26685  1wlkdlem4  28405  nmooval  29026  hiidge0  29361  hommval  29999  hfmmval  30002  nmcfnlbi  30315  mdslmd1i  30592  mdslmd3i  30595  sumdmdlem2  30682  foresf1o  30751  disjdifprg  30815  cnvoprabOLD  30957  xdivval  31095  nsgqusf1olem2  31501  esumfsupre  31939  dya2iocnei  32149  eulerpartlemgc  32229  eulerpartlemb  32235  eulerpartlemgh  32245  ballotlemfc0  32359  ballotlemfcc  32360  subfacp1lem5  33046  subfacp1lem6  33047  cvmliftlem10  33156  elmrsubrn  33382  poxp2  33717  xpord3pred  33725  sexp3  33726  colinearperm1  34291  colinearperm5  34295  endofsegid  34314  segcon2  34334  seglecgr12im  34339  segletr  34343  colinbtwnle  34347  broutsideof2  34351  btwnoutside  34354  outsideoftr  34358  outsidele  34361  opnbnd  34441  ctbssinf  35504  matunitlindf  35702  poimirlem11  35715  poimirlem12  35716  poimirlem16  35720  poimirlem19  35723  poimirlem26  35730  heibor1lem  35894  heiborlem3  35898  heiborlem10  35905  ablo4pnp  35965  crngm4  36088  lkrpssN  37104  pclvalN  37831  polvalN  37846  lclkrlem2x  39471  hgmaprnlem5N  39841  fsuppssindlem1  40203  infdesc  40396  dvgrat  41819  radcnvrat  41821  cncfiooicclem1  43324  fourierdlem101  43638  etransclem24  43689  ioorrnopn  43736  isthincd2  46207