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  935  bm1.1  2162  eqtr3  2197  elnelne1  2451  elnelne2  2452  morex  2921  reuss2  3415  reupick  3419  rabsneu  3665  opabss  4065  triun  4112  poirr  4305  wepo  4357  wetrep  4358  rexxfrd  4461  reg3exmidlemwe  4576  nnsuc  4613  fnfco  5387  fun11iun  5479  fnressn  5699  fvpr1g  5719  fvtp1g  5721  fvtp3g  5723  fvtp3  5726  f1mpt  5767  caovlem2d  6062  offval  6085  dfoprab3  6187  1stconst  6217  2ndconst  6218  poxp  6228  tfrlemisucaccv  6321  tfr1onlemsucaccv  6337  tfrcllemsucaccv  6350  fiintim  6923  addclpi  7321  addnidpig  7330  reapmul1  8546  nnnn0addcl  9200  un0addcl  9203  un0mulcl  9204  zltnle  9293  nn0ge0div  9334  uzind3  9360  uzind4  9582  ltsubrp  9684  ltaddrp  9685  xrlttr  9789  xrltso  9790  xltnegi  9829  xaddnemnf  9851  xaddnepnf  9852  xaddcom  9855  xnegdi  9862  xsubge0  9875  fzind2  10232  qltnle  10239  qbtwnxr  10251  exp3vallem  10514  expp1  10520  expnegap0  10521  expcllem  10524  mulexpzap  10553  expaddzap  10557  expmulzap  10559  hashunlem  10775  shftf  10830  sqrtdiv  11042  mulcn2  11311  summodclem2  11381  fsum3  11386  cvgratz  11531  prodmodclem2  11576  zproddc  11578  prodsnf  11591  dvdsflip  11847  dvdsfac  11856  lcmgcdlem  12067  rpexp1i  12144  hashdvds  12211  hashgcdlem  12228  phisum  12230  pcqcl  12296  pcid  12313  ssnnctlemct  12437  issubmd  12793  grpinvnzcl  12870  mulgneg  12929  mulgnn0z  12937  01eq0ring  13229  lmss  13528  xmetrtri  13658  blssioo  13827  divcnap  13837  dedekindicc  13893  dvidlemap  13942  dvrecap  13959  dveflem  13969  lgsval3  14201  lgsdir2  14216  2sqlem6  14238  bj-bdfindes  14472  bj-findes  14504