Theorem sylan2b 285

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 119	. 2 ⊢ (𝜑 → 𝜒)
3		sylan2b.2	. 2 ⊢ ((𝜓 ∧ 𝜒) → 𝜃)
4	2, 3	sylan2 284	1 ⊢ ((𝜓 ∧ 𝜑) → 𝜃)

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

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

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  syl2anb  289  dcor  920  bm1.1  2142  eqtr3  2177  elnelne1  2431  elnelne2  2432  morex  2896  reuss2  3387  reupick  3391  rabsneu  3632  opabss  4028  triun  4075  poirr  4266  wepo  4318  wetrep  4319  rexxfrd  4421  reg3exmidlemwe  4536  nnsuc  4573  fnfco  5341  fun11iun  5432  fnressn  5650  fvpr1g  5670  fvtp1g  5672  fvtp3g  5674  fvtp3  5677  f1mpt  5716  caovlem2d  6007  offval  6033  dfoprab3  6133  1stconst  6162  2ndconst  6163  poxp  6173  tfrlemisucaccv  6266  tfr1onlemsucaccv  6282  tfrcllemsucaccv  6295  fiintim  6866  addclpi  7230  addnidpig  7239  reapmul1  8453  nnnn0addcl  9103  un0addcl  9106  un0mulcl  9107  zltnle  9196  nn0ge0div  9234  uzind3  9260  uzind4  9482  ltsubrp  9579  ltaddrp  9580  xrlttr  9684  xrltso  9685  xltnegi  9721  xaddnemnf  9743  xaddnepnf  9744  xaddcom  9747  xnegdi  9754  xsubge0  9767  fzind2  10120  qltnle  10127  qbtwnxr  10139  exp3vallem  10402  expp1  10408  expnegap0  10409  expcllem  10412  mulexpzap  10441  expaddzap  10445  expmulzap  10447  hashunlem  10660  shftf  10712  sqrtdiv  10924  mulcn2  11191  summodclem2  11261  fsum3  11266  cvgratz  11411  prodmodclem2  11456  zproddc  11458  prodsnf  11471  dvdsflip  11724  dvdsfac  11733  lcmgcdlem  11934  rpexp1i  12008  hashdvds  12073  hashgcdlem  12090  phisum  12092  lmss  12606  xmetrtri  12736  blssioo  12905  divcnap  12915  dedekindicc  12971  dvidlemap  13020  dvrecap  13037  dveflem  13047  bj-bdfindes  13484  bj-findes  13516