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  rmob  3837  sspsstr  4057  disjne  4404  rexopabb  5473  seex  5580  xpcan2  6132  tron  6337  fcof  6682  fssres  6697  funbrfvb  6884  funopfvb  6885  fvco  6929  fvimacnvi  6994  ffvresb  7067  funressn  7101  funresdfunsn  7132  fvtp2  7139  fvtp2g  7142  fnex  7160  funex  7162  ordsucss  7757  ordsucelsuc  7761  1st2nd  7980  1stconst  8039  2ndconst  8040  frxp  8065  imacosupp  8148  dftpos4  8184  tz7.48lem  8369  nnmsucr  8549  nnmcan  8558  xpmapenlem  9068  php  9127  php4  9130  isfinite2  9193  imafiOLD  9211  fundmfibi  9231  fiinfcl  9398  wofib  9442  r1limg  9675  r1pwcl  9751  cardmin2  9903  zornn0g  10407  mptct  10440  intgru  10716  supsrlem  11013  nzadd  12530  fnn0ind  12582  uztrn2  12761  nnwo  12817  irradd  12877  qbtwnxr  13106  xltnegi  13122  xaddnemnf  13142  xaddnepnf  13143  xaddcom  13146  xnegdi  13154  elioore  13282  uzsubsubfz1  13454  fzo1fzo0n0  13622  elfzonelfzo  13676  modsumfzodifsn  13858  leexp2  14085  faclbnd  14204  faclbnd3  14206  fi1uzind  14421  brfi1uzind  14422  opfi1uzind  14425  swrdccat3b  14654  dvdslelem  16227  divalglem1  16312  dvdsprime  16605  pcgcd  16797  cntri  19252  cntzsgrpcl  19254  efgsrel  19654  xrsdsreclb  21359  znf1o  21497  restuni  23097  stoig  23098  restperf  23119  resstps  23122  pnfnei  23155  mnfnei  23156  cnnei  23217  cmpsublem  23334  comppfsc  23467  tx1stc  23585  xkopt  23590  isfcls  23944  tgioo  24731  opnreen  24767  iscmet3  25240  dyaddisj  25544  limcmpt  25831  degltlem1  26024  ulmdvlem3  26358  lgsdi  27292  noreson  27619  divsclw  28154  cusgrres  29448  crctcshwlkn0lem4  29812  crctcshwlkn0lem5  29813  wwlksnred  29891  eupth2lem3lem4  30232  grpoidinvlem3  30507  ipasslem3  30834  spanuni  31545  5oalem3  31657  5oalem5  31659  mdslmd1lem2  32327  rnressnsn  32682  mptctf  32723  xaddeq0  32761  xnn0gt0  32777  ssdifidllem  33465  ssmxidllem  33482  ssmxidl  33483  ordtconnlem1  34009  esumcvg  34171  ldgenpisyslem1  34248  measdivcst  34309  measdivcstALTV  34310  probun  34504  fnrelpredd  35174  elwf  35180  r1omhf  35189  fineqvrep  35209  elmpps  35689  dfon2lem9  35905  funpartfun  36059  cgrxfr  36171  segcon2  36221  brsegle2  36225  seglecgr12im  36226  segletr  36230  nn0prpw  36439  bj-seex  37039  bj-prmoore  37232  fvineqsneu  37528  lindsenlbs  37728  matunitlindflem2  37730  ptrecube  37733  poimirlem28  37761  ftc1anclem5  37810  ftc1anc  37814  exlimddvfi  38235  imadomfi  42168  readvrec  42532  nn0addcom  42632  nn0mulcom  42636  riccrng1  42691  ricdrng1  42698  mzpclall  42884  4an31  44655  cnrefiisplem  45989  iundjiun  46620  funbrafvb  47318  funopafvb  47319  afvco2  47338  dfatbrafv2b  47407  funbrafv22b  47412  funopafv2b  47413  sprsymrelfolem2  47655  uhgrimgrlim  48149  line2xlem  48915  itsclc0xyqsol  48930  f1mo  49014  catprs  49172  setrec2lem2  49855