Theorem sylanb 592

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

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  syl2anb  609  anabsan  677  rmob  3852  sspsstr  4071  disjne  4418  rexopabb  5510  seex  5618  xpcan2  6174  tron  6380  fcof  6727  fssres  6742  funbrfvb  6932  funopfvb  6933  fvco  6977  fvimacnvi  7045  ffvresb  7119  funressn  7154  funresdfunsn  7185  fvtp2  7192  fvtp2g  7195  fnex  7213  funex  7215  ordsucss  7810  ordsucelsuc  7814  1st2nd  8032  1stconst  8091  2ndconst  8092  frxp  8118  imacosupp  8201  dftpos4  8237  tz7.48lem  8424  nnmsucr  8607  nnmcan  8616  xpmapenlem  9128  php  9187  php4  9190  isfinite2  9254  fundmfibi  9289  fiinfcl  9459  wofib  9503  r1limg  9739  r1pwcl  9815  cardmin2  9981  zornn0g  10485  mptct  10518  intgru  10795  supsrlem  11092  nzadd  12638  fnn0ind  12691  uztrn2  12877  nnwo  12933  irradd  12993  qbtwnxr  13222  xltnegi  13238  xaddnemnf  13258  xaddnepnf  13259  xaddcom  13262  xnegdi  13270  elioore  13398  uzsubsubfz1  13571  fzo1fzo0n0  13740  elfzonelfzo  13794  modsumfzodifsn  13976  leexp2  14203  faclbnd  14322  faclbnd3  14324  fi1uzind  14540  brfi1uzind  14541  opfi1uzind  14544  swrdccat3b  14773  dvdslelem  16363  divalglem1  16448  dvdsprime  16741  pcgcd  16934  cntri  19398  cntzsgrpcl  19400  efgsrel  19800  ssdifidllem  21449  xrsdsreclb  21529  znf1o  21666  restuni  23284  stoig  23285  restperf  23306  resstps  23309  pnfnei  23342  mnfnei  23343  cnnei  23404  cmpsublem  23521  comppfsc  23654  tx1stc  23772  xkopt  23777  isfcls  24131  tgioo  24918  opnreen  24954  iscmet3  25417  dyaddisj  25720  limcmpt  26007  degltlem1  26194  ulmdvlem3  26527  lgsdi  27460  noreson  27786  divsclw  28350  cusgrres  29735  crctcshwlkn0lem4  30099  crctcshwlkn0lem5  30100  wwlksnred  30178  eupth2lem3lem4  30519  grpoidinvlem3  30795  ipasslem3  31122  spanuni  31833  5oalem3  31945  5oalem5  31947  mdslmd1lem2  32615  rnressnsn  32959  mptctf  32998  xaddeq0  33035  xnn0gt0  33051  ssmxidllem  33697  ssmxidl  33698  ordtconnlem1  34255  esumcvg  34417  ldgenpisyslem1  34494  measdivcst  34555  measdivcstALTV  34556  probun  34750  fnrelpredd  35421  elwf  35429  r1omhf  35438  fineqvrep  35446  elmpps  35960  dfon2lem9  36176  funpartfun  36330  cgrxfr  36442  segcon2  36492  brsegle2  36496  seglecgr12im  36497  segletr  36501  nn0prpw  36719  bj-seex  37442  bj-axreprepsep  37595  bj-prmoore  37640  fvineqsneu  37940  lindsenlbs  38149  matunitlindflem2  38151  ptrecube  38154  poimirlem28  38182  ftc1anclem5  38231  ftc1anc  38235  exlimddvfi  38656  imadomfi  42654  readvrec  43006  nn0addcom  43119  nn0mulcom  43123  riccrng1  43174  ricdrng1  43181  mzpclall  43343  4an31  45092  cnrefiisplem  46428  iundjiun  47059  funbrafvb  47775  funopafvb  47776  afvco2  47795  dfatbrafv2b  47864  funbrafv22b  47869  funopafv2b  47870  sprsymrelfolem2  48124  uhgrimgrlim  48634  line2xlem  49411  itsclc0xyqsol  49426  f1mo  49509  catprs  49667  setrec2lem2  50350