Theorem sylanb 581

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 216	. 2 ⊢ (𝜑 → 𝜓)
3		sylanb.2	. 2 ⊢ ((𝜓 ∧ 𝜒) → 𝜃)
4	2, 3	sylan 580	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:  syl2anb  598  anabsan  665  eqtr2OLD  2762  pm13.181OLD  3024  rmob  3890  sspsstr  4108  disjne  4455  rexopabb  5533  seex  5644  xpcan2  6197  tron  6407  fcof  6759  fssres  6774  funbrfvb  6962  funopfvb  6963  fvco  7007  fvimacnvi  7072  ffvresb  7145  funressn  7179  funresdfunsn  7209  fvtp2  7216  fvtp2g  7219  fnex  7237  funex  7239  ordsucss  7838  ordsucelsuc  7842  1st2nd  8064  1stconst  8125  2ndconst  8126  frxp  8151  imacosupp  8234  dftpos4  8270  tz7.48lem  8481  nnmsucr  8663  nnmcan  8672  xpmapenlem  9184  php  9247  php4  9250  phpOLD  9259  isfinite2  9334  imafiOLD  9354  fundmfibi  9376  fiinfcl  9541  wofib  9585  r1limg  9811  r1pwcl  9887  cardmin2  10039  zornn0g  10545  mptct  10578  intgru  10854  supsrlem  11151  nzadd  12665  fnn0ind  12717  uztrn2  12897  nnwo  12955  irradd  13015  qbtwnxr  13242  xltnegi  13258  xaddnemnf  13278  xaddnepnf  13279  xaddcom  13282  xnegdi  13290  elioore  13417  uzsubsubfz1  13587  fzo1fzo0n0  13754  elfzonelfzo  13808  modsumfzodifsn  13985  leexp2  14211  faclbnd  14329  faclbnd3  14331  fi1uzind  14546  brfi1uzind  14547  opfi1uzind  14550  swrdccat3b  14778  dvdslelem  16346  divalglem1  16431  dvdsprime  16724  pcgcd  16916  cntri  19350  cntzsgrpcl  19352  efgsrel  19752  xrsdsreclb  21431  znf1o  21570  restuni  23170  stoig  23171  restperf  23192  resstps  23195  pnfnei  23228  mnfnei  23229  cnnei  23290  cmpsublem  23407  comppfsc  23540  tx1stc  23658  xkopt  23663  isfcls  24017  tgioo  24817  opnreen  24853  iscmet3  25327  dyaddisj  25631  limcmpt  25918  degltlem1  26111  ulmdvlem3  26445  lgsdi  27378  noreson  27705  divsclw  28220  cusgrres  29466  crctcshwlkn0lem4  29833  crctcshwlkn0lem5  29834  wwlksnred  29912  eupth2lem3lem4  30250  grpoidinvlem3  30525  ipasslem3  30852  spanuni  31563  5oalem3  31675  5oalem5  31677  mdslmd1lem2  32345  mptctf  32729  xaddeq0  32757  xnn0gt0  32773  ssdifidllem  33484  ssmxidllem  33501  ssmxidl  33502  ordtconnlem1  33923  esumcvg  34087  ldgenpisyslem1  34164  measdivcst  34225  measdivcstALTV  34226  probun  34421  fnrelpredd  35103  fineqvrep  35109  elmpps  35578  dfon2lem9  35792  funpartfun  35944  cgrxfr  36056  segcon2  36106  brsegle2  36110  seglecgr12im  36111  segletr  36115  nn0prpw  36324  bj-seex  36923  bj-prmoore  37116  fvineqsneu  37412  lindsenlbs  37622  matunitlindflem2  37624  ptrecube  37627  poimirlem28  37655  ftc1anclem5  37704  ftc1anc  37708  exlimddvfi  38129  imadomfi  42003  readvrec  42392  nn0addcom  42480  nn0mulcom  42484  riccrng1  42531  ricdrng1  42538  mzpclall  42738  4an31  44518  cnrefiisplem  45844  iundjiun  46475  funbrafvb  47168  funopafvb  47169  afvco2  47188  dfatbrafv2b  47257  funbrafv22b  47262  funopafv2b  47263  sprsymrelfolem2  47480  uhgrimgrlim  47954  line2xlem  48674  itsclc0xyqsol  48689  f1mo  48762  catprs  48900  setrec2lem2  49213