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  944  bm1.1  2219  eqtr3  2254  elnelne1  2518  elnelne2  2519  morex  3004  reuss2  3505  reupick  3509  rabsneu  3769  invdisjrab  4108  opabss  4179  triun  4226  poirr  4433  wepo  4485  wetrep  4486  rexxfrd  4589  reg3exmidlemwe  4706  nnsuc  4743  fnfco  5544  fun11iun  5640  fnressn  5875  fvpr1g  5895  fvtp1g  5897  fvtp3g  5899  fvtp3  5902  f1mpt  5950  caovlem2d  6255  offval  6283  dfoprab3  6398  1stconst  6430  2ndconst  6431  poxp  6441  suppssrst  6474  suppssrgst  6475  tfrlemisucaccv  6569  tfr1onlemsucaccv  6585  tfrcllemsucaccv  6598  fiintim  7204  2omap  7282  pr1or2  7504  addclpi  7658  addnidpig  7667  reapmul1  8886  nnnn0addcl  9543  un0addcl  9546  un0mulcl  9547  zltnle  9640  nn0ge0div  9683  uzind3  9709  uzind4  9938  ltsubrp  10041  ltaddrp  10042  xrlttr  10147  xrltso  10148  xltnegi  10187  xaddnemnf  10209  xaddnepnf  10210  xaddcom  10213  xnegdi  10220  xsubge0  10233  fzind2  10607  qltnle  10627  qbtwnxr  10641  exp3vallem  10926  expp1  10932  expnegap0  10933  expcllem  10936  mulexpzap  10965  expaddzap  10969  expmulzap  10971  hashunlem  11193  cats1un  11438  reuccatpfxs1  11464  shftf  11540  sqrtdiv  11752  mulcn2  12022  summodclem2  12093  fsum3  12098  cvgratz  12243  prodmodclem2  12288  zproddc  12290  prodsnf  12303  dvdsflip  12562  dvdsfac  12571  bitsfzolem  12665  lcmgcdlem  12799  rpexp1i  12876  hashdvds  12943  hashgcdlem  12960  phisum  12963  pcqcl  13029  pcid  13047  ballotfilemfc0  13176  ballotfilemfcc  13177  ssnnctlemct  13281  issubmd  13771  grpinvnzcl  13869  mulgneg  13941  mulgnn0z  13950  01eq0ring  14419  lmss  15223  xmetrtri  15353  blssioo  15530  divcnap  15542  dedekindicc  15610  dvidlemap  15668  dvidrelem  15669  dvidsslem  15670  dvrecap  15690  dveflem  15703  pellexlem3  15959  lgsval3  16003  lgsdir2  16018  2sqlem6  16105  umgredg  16252  umgrpredgv  16254  umgredgne  16257  umgredgnlp  16259  usgredgppren  16304  edgssv2en  16306  uspgredg2vlem  16327  usgredg2vlem1  16329  uhgr0vsize0en  16342  wlkepvtx  16482  bj-bdfindes  16831  bj-findes  16863