Theorem sylan2b 287

Description: A syllogism inference. (Contributed by NM, 21-Apr-1994.)

Hypotheses

Ref	Expression
sylan2b.1	⊢ (𝜑 ↔ 𝜒)
sylan2b.2	⊢ ((𝜓 ∧ 𝜒) → 𝜃)

Assertion

Ref	Expression
sylan2b	⊢ ((𝜓 ∧ 𝜑) → 𝜃)

Proof of Theorem sylan2b

Step	Hyp	Ref	Expression
1		sylan2b.1	. . 3 ⊢ (𝜑 ↔ 𝜒)
2	1	biimpi 120	. 2 ⊢ (𝜑 → 𝜒)
3		sylan2b.2	. 2 ⊢ ((𝜓 ∧ 𝜒) → 𝜃)
4	2, 3	sylan2 286	1 ⊢ ((𝜓 ∧ 𝜑) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 104   ↔ wb 105

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  syl2anb  291  dcor  937  bm1.1  2181  eqtr3  2216  elnelne1  2471  elnelne2  2472  morex  2948  reuss2  3444  reupick  3448  rabsneu  3696  opabss  4098  triun  4145  poirr  4343  wepo  4395  wetrep  4396  rexxfrd  4499  reg3exmidlemwe  4616  nnsuc  4653  fnfco  5435  fun11iun  5528  fnressn  5751  fvpr1g  5771  fvtp1g  5773  fvtp3g  5775  fvtp3  5778  f1mpt  5821  caovlem2d  6120  offval  6147  dfoprab3  6258  1stconst  6288  2ndconst  6289  poxp  6299  tfrlemisucaccv  6392  tfr1onlemsucaccv  6408  tfrcllemsucaccv  6421  fiintim  7001  addclpi  7411  addnidpig  7420  reapmul1  8639  nnnn0addcl  9296  un0addcl  9299  un0mulcl  9300  zltnle  9389  nn0ge0div  9430  uzind3  9456  uzind4  9679  ltsubrp  9782  ltaddrp  9783  xrlttr  9887  xrltso  9888  xltnegi  9927  xaddnemnf  9949  xaddnepnf  9950  xaddcom  9953  xnegdi  9960  xsubge0  9973  fzind2  10332  qltnle  10350  qbtwnxr  10364  exp3vallem  10649  expp1  10655  expnegap0  10656  expcllem  10659  mulexpzap  10688  expaddzap  10692  expmulzap  10694  hashunlem  10913  shftf  11012  sqrtdiv  11224  mulcn2  11494  summodclem2  11564  fsum3  11569  cvgratz  11714  prodmodclem2  11759  zproddc  11761  prodsnf  11774  dvdsflip  12033  dvdsfac  12042  bitsfzolem  12136  lcmgcdlem  12270  rpexp1i  12347  hashdvds  12414  hashgcdlem  12431  phisum  12434  pcqcl  12500  pcid  12518  ssnnctlemct  12688  issubmd  13176  grpinvnzcl  13274  mulgneg  13346  mulgnn0z  13355  01eq0ring  13821  lmss  14566  xmetrtri  14696  blssioo  14873  divcnap  14885  dedekindicc  14953  dvidlemap  15011  dvidrelem  15012  dvidsslem  15013  dvrecap  15033  dveflem  15046  lgsval3  15343  lgsdir2  15358  2sqlem6  15445  bj-bdfindes  15679  bj-findes  15711  2omap  15726