Theorem sylanb 582

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 581	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  599  anabsan  666  rmob  3842  sspsstr  4062  disjne  4409  rexopabb  5484  seex  5591  xpcan2  6143  tron  6348  fcof  6693  fssres  6708  funbrfvb  6895  funopfvb  6896  fvco  6940  fvimacnvi  7006  ffvresb  7080  funressn  7114  funresdfunsn  7145  fvtp2  7152  fvtp2g  7155  fnex  7173  funex  7175  ordsucss  7770  ordsucelsuc  7774  1st2nd  7993  1stconst  8052  2ndconst  8053  frxp  8078  imacosupp  8161  dftpos4  8197  tz7.48lem  8382  nnmsucr  8563  nnmcan  8572  xpmapenlem  9084  php  9143  php4  9146  isfinite2  9210  imafiOLD  9228  fundmfibi  9248  fiinfcl  9418  wofib  9462  r1limg  9695  r1pwcl  9771  cardmin2  9923  zornn0g  10427  mptct  10460  intgru  10737  supsrlem  11034  nzadd  12551  fnn0ind  12603  uztrn2  12782  nnwo  12838  irradd  12898  qbtwnxr  13127  xltnegi  13143  xaddnemnf  13163  xaddnepnf  13164  xaddcom  13167  xnegdi  13175  elioore  13303  uzsubsubfz1  13475  fzo1fzo0n0  13643  elfzonelfzo  13697  modsumfzodifsn  13879  leexp2  14106  faclbnd  14225  faclbnd3  14227  fi1uzind  14442  brfi1uzind  14443  opfi1uzind  14446  swrdccat3b  14675  dvdslelem  16248  divalglem1  16333  dvdsprime  16626  pcgcd  16818  cntri  19273  cntzsgrpcl  19275  efgsrel  19675  xrsdsreclb  21380  znf1o  21518  restuni  23118  stoig  23119  restperf  23140  resstps  23143  pnfnei  23176  mnfnei  23177  cnnei  23238  cmpsublem  23355  comppfsc  23488  tx1stc  23606  xkopt  23611  isfcls  23965  tgioo  24752  opnreen  24788  iscmet3  25261  dyaddisj  25565  limcmpt  25852  degltlem1  26045  ulmdvlem3  26379  lgsdi  27313  noreson  27640  divsclw  28203  cusgrres  29534  crctcshwlkn0lem4  29898  crctcshwlkn0lem5  29899  wwlksnred  29977  eupth2lem3lem4  30318  grpoidinvlem3  30594  ipasslem3  30921  spanuni  31632  5oalem3  31744  5oalem5  31746  mdslmd1lem2  32414  rnressnsn  32767  mptctf  32806  xaddeq0  32844  xnn0gt0  32860  ssdifidllem  33549  ssmxidllem  33566  ssmxidl  33567  ordtconnlem1  34102  esumcvg  34264  ldgenpisyslem1  34341  measdivcst  34402  measdivcstALTV  34403  probun  34597  fnrelpredd  35268  elwf  35274  r1omhf  35283  fineqvrep  35292  elmpps  35789  dfon2lem9  36005  funpartfun  36159  cgrxfr  36271  segcon2  36321  brsegle2  36325  seglecgr12im  36326  segletr  36330  nn0prpw  36539  bj-seex  37170  bj-axreprepsep  37323  bj-prmoore  37368  fvineqsneu  37666  lindsenlbs  37866  matunitlindflem2  37868  ptrecube  37871  poimirlem28  37899  ftc1anclem5  37948  ftc1anc  37952  exlimddvfi  38373  imadomfi  42372  readvrec  42732  nn0addcom  42832  nn0mulcom  42836  riccrng1  42891  ricdrng1  42898  mzpclall  43084  4an31  44854  cnrefiisplem  46187  iundjiun  46818  funbrafvb  47516  funopafvb  47517  afvco2  47536  dfatbrafv2b  47605  funbrafv22b  47610  funopafv2b  47611  sprsymrelfolem2  47853  uhgrimgrlim  48347  line2xlem  49113  itsclc0xyqsol  49128  f1mo  49212  catprs  49370  setrec2lem2  50053