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  938  bm1.1  2191  eqtr3  2226  elnelne1  2481  elnelne2  2482  morex  2959  reuss2  3455  reupick  3459  rabsneu  3708  invdisjrab  4042  opabss  4113  triun  4160  poirr  4359  wepo  4411  wetrep  4412  rexxfrd  4515  reg3exmidlemwe  4632  nnsuc  4669  fnfco  5459  fun11iun  5552  fnressn  5780  fvpr1g  5800  fvtp1g  5802  fvtp3g  5804  fvtp3  5807  f1mpt  5850  caovlem2d  6149  offval  6176  dfoprab3  6287  1stconst  6317  2ndconst  6318  poxp  6328  tfrlemisucaccv  6421  tfr1onlemsucaccv  6437  tfrcllemsucaccv  6450  fiintim  7040  pr1or2  7313  addclpi  7453  addnidpig  7462  reapmul1  8681  nnnn0addcl  9338  un0addcl  9341  un0mulcl  9342  zltnle  9431  nn0ge0div  9473  uzind3  9499  uzind4  9722  ltsubrp  9825  ltaddrp  9826  xrlttr  9930  xrltso  9931  xltnegi  9970  xaddnemnf  9992  xaddnepnf  9993  xaddcom  9996  xnegdi  10003  xsubge0  10016  fzind2  10381  qltnle  10399  qbtwnxr  10413  exp3vallem  10698  expp1  10704  expnegap0  10705  expcllem  10708  mulexpzap  10737  expaddzap  10741  expmulzap  10743  hashunlem  10962  shftf  11191  sqrtdiv  11403  mulcn2  11673  summodclem2  11743  fsum3  11748  cvgratz  11893  prodmodclem2  11938  zproddc  11940  prodsnf  11953  dvdsflip  12212  dvdsfac  12221  bitsfzolem  12315  lcmgcdlem  12449  rpexp1i  12526  hashdvds  12593  hashgcdlem  12610  phisum  12613  pcqcl  12679  pcid  12697  ssnnctlemct  12867  issubmd  13356  grpinvnzcl  13454  mulgneg  13526  mulgnn0z  13535  01eq0ring  14001  lmss  14768  xmetrtri  14898  blssioo  15075  divcnap  15087  dedekindicc  15155  dvidlemap  15213  dvidrelem  15214  dvidsslem  15215  dvrecap  15235  dveflem  15248  lgsval3  15545  lgsdir2  15560  2sqlem6  15647  bj-bdfindes  15999  bj-findes  16031  2omap  16047