Theorem sylan2br 606

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 231	. 2 ⊢ (𝜑 → 𝜒)
3		sylan2br.2	. 2 ⊢ ((𝜓 ∧ 𝜒) → 𝜃)
4	2, 3	sylan2 604	1 ⊢ ((𝜓 ∧ 𝜑) → 𝜃)

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 400

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

This theorem is used by:  syl2anbr  610  pm2.61danel  3078  imainss  6151  funeu2  6562  imadif  6620  fnop  6644  ssimaex  6966  tfindsg2  7854  nn0suc  7887  xpexr2  7912  poxp2  8135  sexp3  8145  extmptsuppeq  8180  suppss  8186  suppss2  8192  frrlem14  8292  wfr3g  8312  smores3  8336  tfr3ALT  8385  tz7.48-2  8425  swoso  8725  entrfil  9165  domtrfil  9172  1sdom  9211  isinf  9221  frfi  9241  dffi3  9387  marypha1lem  9389  ordtypelem7  9482  cnfcom2lem  9666  r1pw  9813  rankxplim3  9849  dfac5  10117  cofsmo  10257  axcclem  10445  zorn2lem7  10490  wloglei  11750  divval  11878  uzind3  12694  xrltnsym  13166  xaddf  13254  xrsupsslem  13337  xrinfmsslem  13338  0fz1  13576  hashunsng  14433  hashunsngx  14434  hashgt0elexb  14443  sumss  15780  fsumss  15781  fsumcvg3  15785  abscvgcvg  15876  isumshft  15898  geoisum1  15938  geoisum1c  15939  mertenslem2  15944  zprod  15996  prodss  16006  fprodss  16007  rpnnen2lem5  16278  gcdcllem3  16563  lcmgcd  16669  lcmdvds  16670  lcmfval  16683  lcmfcl  16690  dvdslcmf  16693  isprm2lem  16743  eulerthlem2  16845  ramcl2lem  17073  imasvscafn  17595  mreexexlem4d  17707  issgrpd  18792  cycsubgcl  19281  galactghm  19478  odlem2  19613  gexlem2  19656  mulgmhm  19901  mulgghm  19902  gsumval3  19981  gsumpt  20036  dprdfeq0  20098  srglmhm  20307  srgrmhm  20308  ringlghm  20400  ringrghm  20401  sdrgacs  20913  cntzsdrg  20914  lssssr  21084  lbsind  21210  cnsubrg  21586  mplmonmul  22196  mplcoe1  22197  mplcoe5  22200  selvvvval  22302  matplusgcell  22599  elcls  23239  neips  23279  opnnei  23286  ordtbaslem  23354  ptclsg  23781  qtopeu  23882  xmetpsmet  24514  comet  24679  metrest  24690  pcorevlem  25194  dyadmbl  25768  mbfeqalem1  25809  i1fadd  25863  itg1addlem2  25865  itg2uba  25911  itgss  25980  dvcnp  26087  quotval  26462  vieta1lem2  26481  aalioulem3  26506  ulmdvlem3  26574  dvradcnv  26593  abelthlem6  26608  abelthlem9  26612  abelth  26613  logtayllem  26833  logtayl  26834  cxpcl  26848  recxpcl  26849  cxpcn3lem  26921  leibpi  27116  musum  27364  dchrelbas3  27411  sumdchr2  27443  lgscllem  27477  lgsdir2  27503  dchrvmasumiflem2  27675  rpvmasum2  27685  padicabv  27803  padicabvf  27804  padicabvcxp  27805  mulsuniflem  28351  divsval  28391  1wlkdlem4  30500  nmooval  31124  hiidge0  31459  hommval  32097  hfmmval  32100  nmcfnlbi  32413  mdslmd1i  32690  mdslmd3i  32693  sumdmdlem2  32780  foresf1o  32859  disjdifprg  32929  xdivval  33247  nsgqusf1olem2  33732  ply1mulrtss  33881  psrmonmul  33949  esumfsupre  34470  dya2iocnei  34681  eulerpartlemgc  34761  eulerpartlemb  34767  eulerpartlemgh  34777  ballotlemfc0  34892  ballotlemfcc  34893  subfacp1lem5  35684  subfacp1lem6  35685  cvmliftlem10  35794  elmrsubrn  36020  colinearperm1  36562  colinearperm5  36566  endofsegid  36585  segcon2  36605  seglecgr12im  36610  segletr  36614  colinbtwnle  36618  broutsideof2  36622  btwnoutside  36625  outsideoftr  36629  outsidele  36632  opnbnd  36864  ctbssinf  38080  matunitlindf  38297  poimirlem11  38310  poimirlem12  38311  poimirlem16  38315  poimirlem19  38318  poimirlem26  38325  heibor1lem  38488  heiborlem3  38492  heiborlem10  38499  ablo4pnp  38559  crngm4  38682  lkrpssN  39965  pclvalN  40692  polvalN  40707  lclkrlem2x  42332  hgmaprnlem5N  42702  aks6d1c2p2  42914  unitscyglem2  42991  fsuppssindlem1  43351  infdesc  43403  onsupmaxb  43994  dvgrat  45050  radcnvrat  45052  sswfaxreg  45724  cncfiooicclem1  46635  fourierdlem101  46949  etransclem24  47000  ioorrnopn  47047  indprm  48409  isthincd2  50243