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 ⊢ ((𝜓 ∧ 𝜑) → 𝜃)

This proof depends on syntax axioms:   → wi 4   ∧ wa 104   ↔ wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  syl2anb  291  dcor  948  bm1.1  2223  eqtr3  2258  elnelne1  2524  elnelne2  2525  morex  3010  reuss2  3513  reupick  3517  rabsneu  3784  invdisjrab  4124  opabss  4196  triun  4244  poirr  4454  wepo  4506  wetrep  4507  rexxfrd  4611  reg3exmidlemwe  4728  nnsuc  4765  fnfco  5567  fun11iun  5663  fnressn  5904  fvpr1g  5924  fvtp1g  5926  fvtp3g  5928  fvtp3  5931  f1mpt  5980  caovlem2d  6285  offval  6314  dfoprab3  6429  1stconst  6461  2ndconst  6462  poxp  6472  suppssrst  6505  suppssrgst  6506  tfrlemisucaccv  6601  tfr1onlemsucaccv  6617  tfrcllemsucaccv  6630  fiintim  7244  2omap  7325  pr1or2  7547  addclpi  7701  addnidpig  7710  reapmul1  8932  nnnn0addcl  9605  un0addcl  9608  un0mulcl  9609  zltnle  9700  nn0ge0div  9743  uzind3  9770  uzind4  10004  ltsubrp  10108  ltaddrp  10109  xrlttr  10214  xrltso  10215  xltnegi  10254  xaddnemnf  10276  xaddnepnf  10277  xaddcom  10280  xnegdi  10287  xsubge0  10300  fzind2  10675  qltnle  10695  qbtwnxr  10709  exp3vallem  10998  expp1  11004  expnegap0  11005  expcllem  11008  mulexpzap  11037  expaddzap  11041  expmulzap  11043  hashunlem  11266  cats1un  11515  reuccatpfxs1  11541  shftf  11617  sqrtdiv  11830  mulcn2  12103  summodclem2  12174  fsum3  12179  cvgratz  12324  prodmodclem2  12369  zproddc  12371  prodsnf  12384  dvdsflip  12643  dvdsfac  12652  bitsfzolem  12746  lcmgcdlem  12880  rpexp1i  12958  hashdvds  13028  hashgcdlem  13045  phisum  13048  pcqcl  13114  pcid  13132  ballotfilemfc0  13290  ballotfilemfcc  13291  ssnnctlemct  13395  issubmd  13840  grpinvnzcl  13936  mulgneg  14002  mulgnn0z  14011  gsumunsnfd  14259  gsum2dfilem1  14271  gsum2dfilem2  14272  01eq0ring  14605  psrbaglefifi  15175  psrbaglefimap  15183  lmss  15505  xmetrtri  15635  blssioo  15812  divcnap  15824  dedekindicc  15892  dvidlemap  15950  dvidrelem  15951  dvidsslem  15952  dvrecap  15972  dveflem  15985  pellexlem3  16264  prmorcht  16315  lgsval3  16375  lgsdir2  16390  2sqlem6  16477  umgredg  16624  umgrpredgv  16626  umgredgne  16629  umgredgnlp  16631  usgredgppren  16676  edgssv2en  16678  uspgredg2vlem  16699  usgredg2vlem1  16701  uhgr0vsize0en  16714  wlkepvtx  16854  bj-bdfindes  17213  bj-findes  17245