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  936  bm1.1  2173  eqtr3  2208  elnelne1  2463  elnelne2  2464  morex  2935  reuss2  3429  reupick  3433  rabsneu  3679  opabss  4081  triun  4128  poirr  4321  wepo  4373  wetrep  4374  rexxfrd  4477  reg3exmidlemwe  4592  nnsuc  4629  fnfco  5404  fun11iun  5496  fnressn  5717  fvpr1g  5737  fvtp1g  5739  fvtp3g  5741  fvtp3  5744  f1mpt  5787  caovlem2d  6083  offval  6107  dfoprab3  6209  1stconst  6239  2ndconst  6240  poxp  6250  tfrlemisucaccv  6343  tfr1onlemsucaccv  6359  tfrcllemsucaccv  6372  fiintim  6945  addclpi  7343  addnidpig  7352  reapmul1  8569  nnnn0addcl  9223  un0addcl  9226  un0mulcl  9227  zltnle  9316  nn0ge0div  9357  uzind3  9383  uzind4  9605  ltsubrp  9707  ltaddrp  9708  xrlttr  9812  xrltso  9813  xltnegi  9852  xaddnemnf  9874  xaddnepnf  9875  xaddcom  9878  xnegdi  9885  xsubge0  9898  fzind2  10256  qltnle  10263  qbtwnxr  10275  exp3vallem  10538  expp1  10544  expnegap0  10545  expcllem  10548  mulexpzap  10577  expaddzap  10581  expmulzap  10583  hashunlem  10801  shftf  10856  sqrtdiv  11068  mulcn2  11337  summodclem2  11407  fsum3  11412  cvgratz  11557  prodmodclem2  11602  zproddc  11604  prodsnf  11617  dvdsflip  11874  dvdsfac  11883  lcmgcdlem  12094  rpexp1i  12171  hashdvds  12238  hashgcdlem  12255  phisum  12257  pcqcl  12323  pcid  12340  ssnnctlemct  12464  issubmd  12891  grpinvnzcl  12981  mulgneg  13045  mulgnn0z  13054  01eq0ring  13496  lmss  14129  xmetrtri  14259  blssioo  14428  divcnap  14438  dedekindicc  14494  dvidlemap  14543  dvrecap  14560  dveflem  14570  lgsval3  14802  lgsdir2  14817  2sqlem6  14850  bj-bdfindes  15084  bj-findes  15116