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 215	. 2 ⊢ (𝜑 → 𝜓)
3		sylanb.2	. 2 ⊢ ((𝜓 ∧ 𝜒) → 𝜃)
4	2, 3	sylan 580	1 ⊢ ((𝜑 ∧ 𝜒) → 𝜃)

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

This theorem is referenced by:  syl2anb  598  anabsan  662  eqtr2OLD  2764  pm13.181OLD  3028  rmob  3824  sspsstr  4041  disjne  4389  rexopabb  5442  seex  5552  xpcan2  6085  tron  6293  fcof  6632  fssres  6649  funbrfvb  6833  funopfvb  6834  fvco  6875  fvimacnvi  6938  ffvresb  7007  funressn  7040  funresdfunsn  7070  fvtp2  7080  fvtp2g  7083  fnex  7102  funex  7104  ordsucss  7674  ordsucelsuc  7678  1st2nd  7889  1stconst  7949  2ndconst  7950  frxp  7976  imacosupp  8034  dftpos4  8070  tz7.48lem  8281  nnmsucr  8465  nnmcan  8474  xpmapenlem  8940  imafi  8967  php  9002  php4  9005  phpOLD  9014  isfinite2  9081  fundmfibi  9107  fiinfcl  9269  wofib  9313  r1limg  9538  r1pwcl  9614  cardmin2  9766  zornn0g  10270  mptct  10303  intgru  10579  supsrlem  10876  nzadd  12377  fnn0ind  12428  uztrn2  12610  nnwo  12662  irradd  12722  qbtwnxr  12943  xltnegi  12959  xaddnemnf  12979  xaddnepnf  12980  xaddcom  12983  xnegdi  12991  elioore  13118  uzsubsubfz1  13288  fzo1fzo0n0  13447  elfzonelfzo  13498  modsumfzodifsn  13673  leexp2  13898  faclbnd  14013  faclbnd3  14015  fi1uzind  14220  brfi1uzind  14221  opfi1uzind  14224  swrdccat3b  14462  dvdslelem  16027  divalglem1  16112  dvdsprime  16401  pcgcd  16588  cntri  18946  efgsrel  19349  xrsdsreclb  20654  znf1o  20768  restuni  22322  stoig  22323  restperf  22344  resstps  22347  pnfnei  22380  mnfnei  22381  cnnei  22442  cmpsublem  22559  comppfsc  22692  tx1stc  22810  xkopt  22815  isfcls  23169  tgioo  23968  opnreen  24003  iscmet3  24466  dyaddisj  24769  limcmpt  25056  degltlem1  25246  ulmdvlem3  25570  lgsdi  26491  cusgrres  27824  crctcshwlkn0lem4  28187  crctcshwlkn0lem5  28188  wwlksnred  28266  eupth2lem3lem4  28604  grpoidinvlem3  28877  ipasslem3  29204  spanuni  29915  5oalem3  30027  5oalem5  30029  mdslmd1lem2  30697  mptctf  31061  xaddeq0  31085  xnn0gt0  31101  ssmxidllem  31650  ssmxidl  31651  ordtconnlem1  31883  esumcvg  32063  ldgenpisyslem1  32140  measdivcst  32201  measdivcstALTV  32202  probun  32395  fnrelpredd  33070  fineqvrep  33073  elmpps  33544  dfon2lem9  33776  noreson  33872  funpartfun  34254  cgrxfr  34366  segcon2  34416  brsegle2  34420  seglecgr12im  34421  segletr  34425  nn0prpw  34521  bj-seex  35119  bj-prmoore  35295  fvineqsneu  35591  lindsenlbs  35781  matunitlindflem2  35783  ptrecube  35786  poimirlem28  35814  ftc1anclem5  35863  ftc1anc  35867  exlimddvfi  36289  mzpclall  40556  4an31  42125  cnrefiisplem  43377  iundjiun  44005  funbrafvb  44659  funopafvb  44660  afvco2  44679  dfatbrafv2b  44748  funbrafv22b  44753  funopafv2b  44754  sprsymrelfolem2  44956  line2xlem  46110  itsclc0xyqsol  46125  f1mo  46191  catprs  46303  setrec2lem2  46411