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

Syntax hints:   → wi 4   ↔ wb 207   ∧ wa 396

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 208  df-an 397

This theorem is referenced by:  syl2anbr  598  pm2.61danel  3104  imainss  5892  funeu2  6256  imadif  6313  fnop  6335  ssimaex  6620  tfindsg2  7437  nn0suc  7467  xpexr2  7485  extmptsuppeq  7710  suppss  7716  suppss2  7720  wfr3g  7809  smores3  7847  tfr3ALT  7895  tz7.48-2  7934  swoso  8177  isinf  8582  frfi  8614  dffi3  8746  marypha1lem  8748  ordtypelem7  8839  cnfcom2lem  9015  r1pw  9125  rankxplim3  9161  dfac5  9405  cofsmo  9542  axcclem  9730  zorn2lem7  9775  wloglei  11025  divval  11153  uzind3  11930  xrltnsym  12385  xaddf  12472  xrsupsslem  12555  xrinfmsslem  12556  0fz1  12782  hashunsng  13606  hashunsngx  13607  hashgt0elexb  13616  sumss  14919  fsumss  14920  fsumcvg3  14924  abscvgcvg  15012  isumshft  15032  geoisum1  15073  geoisum1c  15074  mertenslem2  15079  zprod  15129  prodss  15139  fprodss  15140  rpnnen2lem5  15409  gcdcllem3  15688  lcmgcd  15785  lcmdvds  15786  lcmfval  15799  lcmfcl  15806  dvdslcmf  15809  isprm2lem  15859  eulerthlem2  15953  ramcl2lem  16179  imasvscafn  16644  mreexexlem4d  16752  cycsubgcl  18064  galactghm  18267  odlem2  18403  gexlem2  18442  mulgmhm  18678  mulgghm  18679  gsumval3  18753  gsumpt  18807  dprdfeq0  18866  srglmhm  18980  srgrmhm  18981  ringlghm  19049  ringrghm  19050  sdrgacs  19275  cntzsdrg  19276  lssssr  19420  lbsind  19547  mplmonmul  19937  mplcoe1  19938  mplcoe5  19941  cnsubrg  20292  matplusgcell  20731  elcls  21370  neips  21410  opnnei  21417  ordtbaslem  21485  ptclsg  21912  qtopeu  22013  xmetpsmet  22646  comet  22811  metrest  22822  pcorevlem  23318  dyadmbl  23889  mbfeqalem1  23930  i1fadd  23984  itg1addlem2  23986  itg2uba  24032  itgss  24100  dvcnp  24204  quotval  24569  vieta1lem2  24588  aalioulem3  24611  ulmdvlem3  24678  dvradcnv  24697  abelthlem6  24712  abelthlem9  24716  abelth  24717  logtayllem  24928  logtayl  24929  cxpcl  24943  recxpcl  24944  cxpcn3lem  25014  leibpi  25207  musum  25455  dchrelbas3  25501  sumdchr2  25533  lgscllem  25567  lgsdir2  25593  dchrvmasumiflem2  25765  rpvmasum2  25775  padicabv  25893  padicabvf  25894  padicabvcxp  25895  1wlkdlem4  27611  nmooval  28236  hiidge0  28571  hommval  29209  hfmmval  29212  nmcfnlbi  29525  mdslmd1i  29802  mdslmd3i  29805  sumdmdlem2  29892  foresf1o  29962  disjdifprg  30020  cnvoprabOLD  30149  xdivval  30284  esumfsupre  30952  dya2iocnei  31162  eulerpartlemgc  31242  eulerpartlemb  31248  eulerpartlemgh  31258  ballotlemfc0  31372  ballotlemfcc  31373  subfacp1lem5  32045  subfacp1lem6  32046  cvmliftlem10  32155  elmrsubrn  32381  frrlem14  32751  colinearperm1  33138  colinearperm5  33142  endofsegid  33161  segcon2  33181  seglecgr12im  33186  segletr  33190  colinbtwnle  33194  broutsideof2  33198  btwnoutside  33201  outsideoftr  33205  outsidele  33208  opnbnd  33288  ctbssinf  34243  matunitlindf  34446  poimirlem11  34459  poimirlem12  34460  poimirlem16  34464  poimirlem19  34467  poimirlem26  34474  heibor1lem  34644  heiborlem3  34648  heiborlem10  34655  ablo4pnp  34715  crngm4  34838  lkrpssN  35855  pclvalN  36582  polvalN  36597  lclkrlem2x  38222  hgmaprnlem5N  38592  dvgrat  40207  radcnvrat  40209  cncfiooicclem1  41743  fourierdlem101  42060  etransclem24  42111  ioorrnopn  42158