Theorem sylan2br 607

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

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

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 402

This theorem is used by:  syl2anbr  611  pm2.61danel  3080  imainss  6153  funeu2  6567  imadif  6625  fnop  6649  ssimaex  6971  tfindsg2  7865  nn0suc  7898  xpexr2  7923  poxp2  8146  sexp3  8156  extmptsuppeq  8191  suppss  8197  suppss2  8203  frrlem14  8303  wfr3g  8323  smores3  8347  tfr3ALT  8396  tz7.48-2  8436  swoso  8736  entrfil  9177  domtrfil  9184  1sdom  9223  isinf  9233  frfi  9253  dffi3  9399  marypha1lem  9401  ordtypelem7  9494  cnfcom2lem  9678  r1pw  9825  rankxplim3  9861  dfac5  10129  cofsmo  10269  axcclem  10457  zorn2lem7  10502  wloglei  11766  divval  11894  uzind3  12711  xrltnsym  13183  xaddf  13271  xrsupsslem  13354  xrinfmsslem  13355  0fz1  13593  hashunsng  14451  hashunsngx  14452  hashgt0elexb  14461  sumss  15803  fsumss  15804  fsumcvg3  15808  abscvgcvg  15899  isumshft  15921  geoisum1  15961  geoisum1c  15962  mertenslem2  15967  zprod  16019  prodss  16029  fprodss  16030  rpnnen2lem5  16301  gcdcllem3  16586  lcmgcd  16692  lcmdvds  16693  lcmfval  16706  lcmfcl  16713  dvdslcmf  16716  isprm2lem  16766  eulerthlem2  16868  ramcl2lem  17096  imasvscafn  17618  mreexexlem4d  17730  issgrpd  18825  cycsubgcl  19326  galactghm  19523  odlem2  19658  gexlem2  19701  mulgmhm  19946  mulgghm  19947  gsumval3  20026  gsumpt  20081  dprdfeq0  20143  srglmhm  20352  srgrmhm  20353  ringlghm  20446  ringrghm  20447  sdrgacs  20959  cntzsdrg  20960  lssssr  21130  lbsind  21256  cnsubrg  21632  mplmonmul  22242  mplcoe1  22243  mplcoe5  22246  selvvvval  22348  matplusgcell  22645  elcls  23285  neips  23325  opnnei  23332  ordtbaslem  23400  ptclsg  23828  qtopeu  23929  xmetpsmet  24561  comet  24726  metrest  24737  pcorevlem  25241  dyadmbl  25815  mbfeqalem1  25856  i1fadd  25910  itg1addlem2  25912  itg2uba  25958  itgss  26027  dvcnp  26134  quotval  26509  vieta1lem2  26528  aalioulem3  26553  ulmdvlem3  26621  dvradcnv  26640  abelthlem6  26655  abelthlem9  26659  abelth  26660  logtayllem  26880  logtayl  26881  cxpcl  26895  recxpcl  26896  cxpcn3lem  26968  leibpi  27163  musum  27411  dchrelbas3  27458  sumdchr2  27490  lgscllem  27524  lgsdir2  27550  dchrvmasumiflem2  27722  rpvmasum2  27732  padicabv  27850  padicabvf  27851  padicabvcxp  27852  mulsuniflem  28398  divsval  28438  1wlkdlem4  30563  nmooval  31191  hiidge0  31526  hommval  32164  hfmmval  32167  nmcfnlbi  32480  mdslmd1i  32757  mdslmd3i  32760  sumdmdlem2  32847  foresf1o  32926  disjdifprg  32996  xdivval  33313  nsgqusf1olem2  33792  ply1mulrtss  33941  psrmonmul  34009  esumfsupre  34530  dya2iocnei  34742  eulerpartlemgc  34822  eulerpartlemb  34828  eulerpartlemgh  34838  ballotlemfc0  34953  ballotlemfcc  34954  subfacp1lem5  35718  subfacp1lem6  35719  cvmliftlem10  35828  elmrsubrn  36054  colinearperm1  36596  colinearperm5  36600  endofsegid  36619  segcon2  36639  seglecgr12im  36644  segletr  36648  colinbtwnle  36652  broutsideof2  36656  btwnoutside  36659  outsideoftr  36663  outsidele  36666  opnbnd  36898  ctbssinf  38114  matunitlindf  38331  poimirlem11  38344  poimirlem12  38345  poimirlem16  38349  poimirlem19  38352  poimirlem26  38359  heibor1lem  38523  heiborlem3  38527  heiborlem10  38534  ablo4pnp  38594  crngm4  38717  lkrpssN  40000  pclvalN  40727  polvalN  40742  lclkrlem2x  42367  hgmaprnlem5N  42737  aks6d1c2p2  42949  unitscyglem2  43026  fsuppssindlem1  43401  infdesc  43453  onsupmaxb  44044  dvgrat  45100  radcnvrat  45102  sswfaxreg  45774  cncfiooicclem1  46685  fourierdlem101  46999  etransclem24  47050  ioorrnopn  47097  indprm  48459  isthincd2  50292