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  6600  tfr1onlemsucaccv  6616  tfrcllemsucaccv  6629  fiintim  7243  2omap  7325  pr1or2  7547  addclpi  7701  addnidpig  7710  reapmul1  8932  nnnn0addcl  9605  un0addcl  9608  un0mulcl  9609  zltnle  9702  nn0ge0div  9745  uzind3  9771  uzind4  10005  ltsubrp  10109  ltaddrp  10110  xrlttr  10215  xrltso  10216  xltnegi  10255  xaddnemnf  10277  xaddnepnf  10278  xaddcom  10281  xnegdi  10288  xsubge0  10301  fzind2  10676  qltnle  10696  qbtwnxr  10710  exp3vallem  10999  expp1  11005  expnegap0  11006  expcllem  11009  mulexpzap  11038  expaddzap  11042  expmulzap  11044  hashunlem  11267  cats1un  11516  reuccatpfxs1  11542  shftf  11618  sqrtdiv  11831  mulcn2  12104  summodclem2  12175  fsum3  12180  cvgratz  12325  prodmodclem2  12370  zproddc  12372  prodsnf  12385  dvdsflip  12644  dvdsfac  12653  bitsfzolem  12747  lcmgcdlem  12881  rpexp1i  12959  hashdvds  13029  hashgcdlem  13046  phisum  13049  pcqcl  13115  pcid  13133  ballotfilemfc0  13291  ballotfilemfcc  13292  ssnnctlemct  13396  issubmd  13841  grpinvnzcl  13937  mulgneg  14003  mulgnn0z  14012  gsumunsnfd  14260  gsum2dfilem1  14272  gsum2dfilem2  14273  01eq0ring  14606  psrbaglefifi  15177  lmss  15484  xmetrtri  15614  blssioo  15791  divcnap  15803  dedekindicc  15871  dvidlemap  15929  dvidrelem  15930  dvidsslem  15931  dvrecap  15951  dveflem  15964  pellexlem3  16243  prmorcht  16294  lgsval3  16354  lgsdir2  16369  2sqlem6  16456  umgredg  16603  umgrpredgv  16605  umgredgne  16608  umgredgnlp  16610  usgredgppren  16655  edgssv2en  16657  uspgredg2vlem  16678  usgredg2vlem1  16680  uhgr0vsize0en  16693  wlkepvtx  16833  bj-bdfindes  17192  bj-findes  17224