Theorem sylanb 580

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 579	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  597  anabsan  664  eqtr2OLD  2765  pm13.181OLD  3030  rmob  3912  sspsstr  4131  disjne  4478  rexopabb  5547  seex  5659  xpcan2  6208  tron  6418  fcof  6770  fssres  6787  funbrfvb  6975  funopfvb  6976  fvco  7020  fvimacnvi  7085  ffvresb  7159  funressn  7193  funresdfunsn  7223  fvtp2  7233  fvtp2g  7236  fnex  7254  funex  7256  ordsucss  7854  ordsucelsuc  7858  1st2nd  8080  1stconst  8141  2ndconst  8142  frxp  8167  imacosupp  8250  dftpos4  8286  tz7.48lem  8497  nnmsucr  8681  nnmcan  8690  xpmapenlem  9210  php  9273  php4  9276  phpOLD  9285  isfinite2  9362  imafiOLD  9382  fundmfibi  9404  fiinfcl  9570  wofib  9614  r1limg  9840  r1pwcl  9916  cardmin2  10068  zornn0g  10574  mptct  10607  intgru  10883  supsrlem  11180  nzadd  12691  fnn0ind  12742  uztrn2  12922  nnwo  12978  irradd  13038  qbtwnxr  13262  xltnegi  13278  xaddnemnf  13298  xaddnepnf  13299  xaddcom  13302  xnegdi  13310  elioore  13437  uzsubsubfz1  13607  fzo1fzo0n0  13767  elfzonelfzo  13819  modsumfzodifsn  13995  leexp2  14221  faclbnd  14339  faclbnd3  14341  fi1uzind  14556  brfi1uzind  14557  opfi1uzind  14560  swrdccat3b  14788  dvdslelem  16357  divalglem1  16442  dvdsprime  16734  pcgcd  16925  cntri  19372  cntzsgrpcl  19374  efgsrel  19776  xrsdsreclb  21454  znf1o  21593  restuni  23191  stoig  23192  restperf  23213  resstps  23216  pnfnei  23249  mnfnei  23250  cnnei  23311  cmpsublem  23428  comppfsc  23561  tx1stc  23679  xkopt  23684  isfcls  24038  tgioo  24837  opnreen  24872  iscmet3  25346  dyaddisj  25650  limcmpt  25938  degltlem1  26131  ulmdvlem3  26463  lgsdi  27396  noreson  27723  divsclw  28238  cusgrres  29484  crctcshwlkn0lem4  29846  crctcshwlkn0lem5  29847  wwlksnred  29925  eupth2lem3lem4  30263  grpoidinvlem3  30538  ipasslem3  30865  spanuni  31576  5oalem3  31688  5oalem5  31690  mdslmd1lem2  32358  mptctf  32731  xaddeq0  32760  xnn0gt0  32776  ssdifidllem  33449  ssmxidllem  33466  ssmxidl  33467  ordtconnlem1  33870  esumcvg  34050  ldgenpisyslem1  34127  measdivcst  34188  measdivcstALTV  34189  probun  34384  fnrelpredd  35065  fineqvrep  35071  elmpps  35541  dfon2lem9  35755  funpartfun  35907  cgrxfr  36019  segcon2  36069  brsegle2  36073  seglecgr12im  36074  segletr  36078  nn0prpw  36289  bj-seex  36888  bj-prmoore  37081  fvineqsneu  37377  lindsenlbs  37575  matunitlindflem2  37577  ptrecube  37580  poimirlem28  37608  ftc1anclem5  37657  ftc1anc  37661  exlimddvfi  38082  imadomfi  41959  nn0addcom  42426  nn0mulcom  42430  riccrng1  42476  ricdrng1  42483  mzpclall  42683  4an31  44469  cnrefiisplem  45750  iundjiun  46381  funbrafvb  47071  funopafvb  47072  afvco2  47091  dfatbrafv2b  47160  funbrafv22b  47165  funopafv2b  47166  sprsymrelfolem2  47367  uhgrimgrlim  47811  line2xlem  48487  itsclc0xyqsol  48502  f1mo  48566  catprs  48678  setrec2lem2  48786