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  2125  eqtr3  2160  elnelne1  2413  elnelne2  2414  morex  2872  reuss2  3361  reupick  3365  rabsneu  3604  opabss  4000  triun  4047  poirr  4237  wepo  4289  wetrep  4290  rexxfrd  4392  reg3exmidlemwe  4501  nnsuc  4537  fnfco  5305  fun11iun  5396  fnressn  5614  fvpr1g  5634  fvtp1g  5636  fvtp3g  5638  fvtp3  5641  f1mpt  5680  caovlem2d  5971  offval  5997  dfoprab3  6097  1stconst  6126  2ndconst  6127  poxp  6137  tfrlemisucaccv  6230  tfr1onlemsucaccv  6246  tfrcllemsucaccv  6259  fiintim  6825  addclpi  7159  addnidpig  7168  reapmul1  8381  nnnn0addcl  9031  un0addcl  9034  un0mulcl  9035  zltnle  9124  nn0ge0div  9162  uzind3  9188  uzind4  9410  ltsubrp  9507  ltaddrp  9508  xrlttr  9611  xrltso  9612  xltnegi  9648  xaddnemnf  9670  xaddnepnf  9671  xaddcom  9674  xnegdi  9681  xsubge0  9694  fzind2  10047  qltnle  10054  qbtwnxr  10066  exp3vallem  10325  expp1  10331  expnegap0  10332  expcllem  10335  mulexpzap  10364  expaddzap  10368  expmulzap  10370  hashunlem  10582  shftf  10634  sqrtdiv  10846  mulcn2  11113  summodclem2  11183  fsum3  11188  cvgratz  11333  prodmodclem2  11378  zproddc  11380  dvdsflip  11585  dvdsfac  11594  lcmgcdlem  11794  rpexp1i  11868  hashdvds  11933  hashgcdlem  11939  lmss  12454  xmetrtri  12584  blssioo  12753  divcnap  12763  dedekindicc  12819  dvidlemap  12868  dvrecap  12885  dveflem  12895  bj-bdfindes  13318  bj-findes  13350