Theorem sylanb 593

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 592	1 ⊢ ((𝜑 ∧ 𝜒) → 𝜃)

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  syl2anb  610  anabsan  678  rmob  3837  sspsstr  4057  disjne  4408  ssexg  5281  rexopabb  5502  seex  5610  xpcan2  6169  tron  6384  fcof  6731  fssres  6746  funbrfvb  6936  funopfvb  6937  fvco  6981  fvimacnvi  7049  ffvresb  7124  funressn  7161  funresdfunsn  7192  fvtp2  7199  fvtp2g  7202  fnex  7221  funex  7223  ordsucss  7827  ordsucelsuc  7831  1st2nd  8048  1stconst  8109  2ndconst  8110  frxp  8136  imacosupp  8219  dftpos4  8255  tz7.48lemOLD  8444  nnmsucr  8627  nnmcan  8636  xpmapenlem  9156  php  9215  php4  9218  isfinite2  9283  fundmfibi  9318  fiinfcl  9488  wofib  9532  r1limg  9771  elwf  9835  r1pwcl  9854  setrec2lem2  9969  cardmin2  10073  zornn0g  10576  mptct  10615  intgru  10892  supsrlem  11189  nzadd  12737  fnn0ind  12791  uztrn2  12977  nnwo  13033  irradd  13094  qbtwnxr  13323  xltnegi  13339  xaddnemnf  13359  xaddnepnf  13360  xaddcom  13363  xnegdi  13371  elioore  13499  uzsubsubfz1  13674  fzo1fzo0n0  13843  elfzonelfzo  13897  modsumfzodifsn  14080  leexp2  14307  faclbnd  14427  faclbnd3  14429  fi1uzind  14645  brfi1uzind  14646  opfi1uzind  14649  swrdccat3b  14882  dvdslelem  16472  divalglem1  16557  dvdsprime  16855  pcgcd  17049  cntri  19539  cntzsgrpcl  19541  efgsrel  19941  ssdifidllem  21633  xrsdsreclb  21713  znf1o  21850  lindsenlbs  22150  matunitlindflem2  22988  restuni  23473  stoig  23474  restperf  23495  resstps  23498  pnfnei  23531  mnfnei  23532  cnnei  23593  cmpsublem  23710  comppfsc  23844  tx1stc  23962  xkopt  23967  isfcls  24321  tgioo  25108  opnreen  25144  iscmet3  25607  dyaddisj  25910  limcmpt  26196  degltlem1  26383  ulmdvlem3  26722  lgsdi  27654  noreson  28010  divsclw  28574  cusgrres  30022  crctcshwlkn0lem4  30395  crctcshwlkn0lem5  30396  wwlksnred  30474  eupth2lem3lem4  30825  grpoidinvlem3  31101  ipasslem3  31428  spanuni  32139  5oalem3  32251  5oalem5  32253  mdslmd1lem2  32921  rnressnsn  33264  mptctf  33301  xaddeq0  33338  xnn0gt0  33354  ssmxidllem  33991  ssmxidl  33992  ordtconnlem1  34549  esumcvg  34711  ldgenpisyslem1  34789  measdivcst  34850  measdivcstALTV  34851  probun  35044  fnrelpredd  35709  fineqvrep  35765  elmpps  36317  dfon2lem9  36533  funpartfun  36687  cgrxfr  36800  segcon2  36850  brsegle2  36854  seglecgr12im  36855  segletr  36859  nn0prpw  37091  mh-inf3f1  37309  bj-seex  37814  bj-axreprepsep  37971  bj-prmoore  38016  fvineqsneu  38314  ptrecube  38518  poimirlem28  38546  ftc1anclem5  38595  ftc1anc  38599  exlimddvfi  39034  imadomfi  43032  readvrec  43393  nn0addcom  43506  nn0mulcom  43510  riccrng1  43562  ricdrng1  43572  mzpclall  43717  4an31  45466  cnrefiisplem  46808  iundjiun  47439  funbrafvb  48195  funopafvb  48196  afvco2  48215  dfatbrafv2b  48284  funbrafv22b  48289  funopafv2b  48290  sprsymrelfolem2  48544  uhgrimgrlim  49054  line2xlem  49834  itsclc0xyqsol  49849  f1mo  49932  catprs  50088