Theorem sylanb 587

Description: A syllogism inference. (Contributed by NM, 18-May-1994.)

Hypotheses

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

Assertion

Ref	Expression
sylanb	⊢ ((𝜑 ∧ 𝜒) → 𝜃)

Proof of Theorem sylanb

Step	Hyp	Ref	Expression
1		sylanb.1	. . 3 ⊢ (𝜑 ↔ 𝜓)
2	1	biimpi 217	. 2 ⊢ (𝜑 → 𝜓)
3		sylanb.2	. 2 ⊢ ((𝜓 ∧ 𝜒) → 𝜃)
4	2, 3	sylan 586	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:  syl2anb  604  anabsan  671  rmob  3822  sspsstr  4039  disjne  4383  rexopabb  5470  seex  5577  xpcan2  6128  tron  6333  fcof  6678  fssres  6693  funbrfvb  6880  funopfvb  6881  fvco  6925  fvimacnvi  6993  ffvresb  7067  funressn  7102  funresdfunsn  7133  fvtp2  7140  fvtp2g  7143  fnex  7161  funex  7163  ordsucss  7758  ordsucelsuc  7762  1st2nd  7981  1stconst  8039  2ndconst  8040  frxp  8066  imacosupp  8149  dftpos4  8185  tz7.48lem  8370  nnmsucr  8551  nnmcan  8560  xpmapenlem  9072  php  9131  php4  9134  isfinite2  9198  imafiOLD  9216  fundmfibi  9236  fiinfcl  9406  wofib  9450  r1limg  9686  r1pwcl  9762  cardmin2  9914  zornn0g  10418  mptct  10451  intgru  10728  supsrlem  11025  nzadd  12566  fnn0ind  12619  uztrn2  12798  nnwo  12854  irradd  12914  qbtwnxr  13143  xltnegi  13159  xaddnemnf  13179  xaddnepnf  13180  xaddcom  13183  xnegdi  13191  elioore  13319  uzsubsubfz1  13492  fzo1fzo0n0  13661  elfzonelfzo  13715  modsumfzodifsn  13897  leexp2  14124  faclbnd  14243  faclbnd3  14245  fi1uzind  14460  brfi1uzind  14461  opfi1uzind  14464  swrdccat3b  14693  dvdslelem  16269  divalglem1  16354  dvdsprime  16647  pcgcd  16840  cntri  19298  cntzsgrpcl  19300  efgsrel  19700  xrsdsreclb  21389  znf1o  21526  restuni  23145  stoig  23146  restperf  23167  resstps  23170  pnfnei  23203  mnfnei  23204  cnnei  23265  cmpsublem  23382  comppfsc  23515  tx1stc  23633  xkopt  23638  isfcls  23992  tgioo  24779  opnreen  24815  iscmet3  25278  dyaddisj  25581  limcmpt  25868  degltlem1  26055  ulmdvlem3  26385  lgsdi  27315  noreson  27642  divsclw  28205  cusgrres  29535  crctcshwlkn0lem4  29899  crctcshwlkn0lem5  29900  wwlksnred  29978  eupth2lem3lem4  30319  grpoidinvlem3  30595  ipasslem3  30922  spanuni  31633  5oalem3  31745  5oalem5  31747  mdslmd1lem2  32415  rnressnsn  32769  mptctf  32808  xaddeq0  32845  xnn0gt0  32861  ssdifidllem  33539  ssmxidllem  33556  ssmxidl  33557  ordtconnlem1  34108  esumcvg  34270  ldgenpisyslem1  34347  measdivcst  34408  measdivcstALTV  34409  probun  34603  fnrelpredd  35272  elwf  35278  r1omhf  35287  fineqvrep  35295  elmpps  35801  dfon2lem9  36017  funpartfun  36171  cgrxfr  36283  segcon2  36333  brsegle2  36337  seglecgr12im  36338  segletr  36342  nn0prpw  36551  bj-seex  37275  bj-axreprepsep  37428  bj-prmoore  37473  fvineqsneu  37773  lindsenlbs  37982  matunitlindflem2  37984  ptrecube  37987  poimirlem28  38015  ftc1anclem5  38064  ftc1anc  38068  exlimddvfi  38489  imadomfi  42487  readvrec  42839  nn0addcom  42952  nn0mulcom  42956  riccrng1  43007  ricdrng1  43014  mzpclall  43176  4an31  44942  cnrefiisplem  46272  iundjiun  46903  funbrafvb  47619  funopafvb  47620  afvco2  47639  dfatbrafv2b  47708  funbrafv22b  47713  funopafv2b  47714  sprsymrelfolem2  47968  uhgrimgrlim  48478  line2xlem  49244  itsclc0xyqsol  49259  f1mo  49343  catprs  49501  setrec2lem2  50184