Theorem sylan2br 595

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ 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 207  df-an 396

This theorem is referenced by:  syl2anbr  599  pm2.61danel  3051  imainss  6148  funeu2  6567  imadif  6625  fnop  6652  ssimaex  6969  tfindsg2  7862  nn0suc  7895  xpexr2  7920  poxp2  8147  sexp3  8157  extmptsuppeq  8192  suppss  8198  suppss2  8204  frrlem14  8303  wfr3g  8326  smores3  8372  tfr3ALT  8421  tz7.48-2  8461  swoso  8758  entrfil  9204  domtrfil  9211  1sdom  9261  isinf  9273  isinfOLD  9274  frfi  9298  dffi3  9448  marypha1lem  9450  ordtypelem7  9543  cnfcom2lem  9720  r1pw  9864  rankxplim3  9900  dfac5  10148  cofsmo  10288  axcclem  10476  zorn2lem7  10521  wloglei  11774  divval  11903  uzind3  12692  xrltnsym  13158  xaddf  13245  xrsupsslem  13328  xrinfmsslem  13329  0fz1  13566  hashunsng  14415  hashunsngx  14416  hashgt0elexb  14425  sumss  15745  fsumss  15746  fsumcvg3  15750  abscvgcvg  15840  isumshft  15860  geoisum1  15900  geoisum1c  15901  mertenslem2  15906  zprod  15958  prodss  15968  fprodss  15969  rpnnen2lem5  16241  gcdcllem3  16525  lcmgcd  16631  lcmdvds  16632  lcmfval  16645  lcmfcl  16652  dvdslcmf  16655  isprm2lem  16705  eulerthlem2  16806  ramcl2lem  17034  imasvscafn  17556  mreexexlem4d  17664  issgrpd  18713  cycsubgcl  19194  galactghm  19390  odlem2  19525  gexlem2  19568  mulgmhm  19813  mulgghm  19814  gsumval3  19893  gsumpt  19948  dprdfeq0  20010  srglmhm  20186  srgrmhm  20187  ringlghm  20277  ringrghm  20278  sdrgacs  20766  cntzsdrg  20767  lssssr  20916  lbsind  21043  cnsubrg  21400  mplmonmul  21999  mplcoe1  22000  mplcoe5  22003  matplusgcell  22376  elcls  23016  neips  23056  opnnei  23063  ordtbaslem  23131  ptclsg  23558  qtopeu  23659  xmetpsmet  24292  comet  24457  metrest  24468  pcorevlem  24982  dyadmbl  25558  mbfeqalem1  25599  i1fadd  25653  itg1addlem2  25655  itg2uba  25701  itgss  25770  dvcnp  25877  quotval  26257  vieta1lem2  26276  aalioulem3  26299  ulmdvlem3  26368  dvradcnv  26387  abelthlem6  26403  abelthlem9  26407  abelth  26408  logtayllem  26625  logtayl  26626  cxpcl  26640  recxpcl  26641  cxpcn3lem  26714  leibpi  26909  musum  27158  dchrelbas3  27206  sumdchr2  27238  lgscllem  27272  lgsdir2  27298  dchrvmasumiflem2  27470  rpvmasum2  27480  padicabv  27598  padicabvf  27599  padicabvcxp  27600  mulsuniflem  28109  divsval  28149  1wlkdlem4  30126  nmooval  30749  hiidge0  31084  hommval  31722  hfmmval  31725  nmcfnlbi  32038  mdslmd1i  32315  mdslmd3i  32318  sumdmdlem2  32405  foresf1o  32490  disjdifprg  32561  xdivval  32898  nsgqusf1olem2  33434  ply1mulrtss  33599  esumfsupre  34107  dya2iocnei  34319  eulerpartlemgc  34399  eulerpartlemb  34405  eulerpartlemgh  34415  ballotlemfc0  34530  ballotlemfcc  34531  subfacp1lem5  35211  subfacp1lem6  35212  cvmliftlem10  35321  elmrsubrn  35547  colinearperm1  36085  colinearperm5  36089  endofsegid  36108  segcon2  36128  seglecgr12im  36133  segletr  36137  colinbtwnle  36141  broutsideof2  36145  btwnoutside  36148  outsideoftr  36152  outsidele  36155  opnbnd  36348  ctbssinf  37429  matunitlindf  37647  poimirlem11  37660  poimirlem12  37661  poimirlem16  37665  poimirlem19  37668  poimirlem26  37675  heibor1lem  37838  heiborlem3  37842  heiborlem10  37849  ablo4pnp  37909  crngm4  38032  lkrpssN  39186  pclvalN  39914  polvalN  39929  lclkrlem2x  41554  hgmaprnlem5N  41924  aks6d1c2p2  42137  unitscyglem2  42214  selvvvval  42583  fsuppssindlem1  42589  infdesc  42641  onsupmaxb  43238  dvgrat  44311  radcnvrat  44313  sswfaxreg  44987  cncfiooicclem1  45902  fourierdlem101  46216  etransclem24  46267  ioorrnopn  46314  isthincd2  49303