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  2216  eqtr3  2251  elnelne1  2507  elnelne2  2508  morex  2991  reuss2  3489  reupick  3493  rabsneu  3748  invdisjrab  4087  opabss  4158  triun  4205  poirr  4410  wepo  4462  wetrep  4463  rexxfrd  4566  reg3exmidlemwe  4683  nnsuc  4720  fnfco  5519  fun11iun  5613  fnressn  5848  fvpr1g  5868  fvtp1g  5870  fvtp3g  5872  fvtp3  5875  f1mpt  5922  caovlem2d  6225  offval  6252  dfoprab3  6363  1stconst  6395  2ndconst  6396  poxp  6406  suppssrst  6439  suppssrgst  6440  tfrlemisucaccv  6534  tfr1onlemsucaccv  6550  tfrcllemsucaccv  6563  fiintim  7166  pr1or2  7442  addclpi  7590  addnidpig  7599  reapmul1  8818  nnnn0addcl  9475  un0addcl  9478  un0mulcl  9479  zltnle  9568  nn0ge0div  9610  uzind3  9636  uzind4  9865  ltsubrp  9968  ltaddrp  9969  xrlttr  10073  xrltso  10074  xltnegi  10113  xaddnemnf  10135  xaddnepnf  10136  xaddcom  10139  xnegdi  10146  xsubge0  10159  fzind2  10529  qltnle  10547  qbtwnxr  10561  exp3vallem  10846  expp1  10852  expnegap0  10853  expcllem  10856  mulexpzap  10885  expaddzap  10889  expmulzap  10891  hashunlem  11111  cats1un  11349  reuccatpfxs1  11375  shftf  11451  sqrtdiv  11663  mulcn2  11933  summodclem2  12004  fsum3  12009  cvgratz  12154  prodmodclem2  12199  zproddc  12201  prodsnf  12214  dvdsflip  12473  dvdsfac  12482  bitsfzolem  12576  lcmgcdlem  12710  rpexp1i  12787  hashdvds  12854  hashgcdlem  12871  phisum  12874  pcqcl  12940  pcid  12958  ssnnctlemct  13128  issubmd  13618  grpinvnzcl  13716  mulgneg  13788  mulgnn0z  13797  01eq0ring  14265  lmss  15037  xmetrtri  15167  blssioo  15344  divcnap  15356  dedekindicc  15424  dvidlemap  15482  dvidrelem  15483  dvidsslem  15484  dvrecap  15504  dveflem  15517  pellexlem3  15773  lgsval3  15817  lgsdir2  15832  2sqlem6  15919  umgredg  16066  umgrpredgv  16068  umgredgne  16071  umgredgnlp  16073  usgredgppren  16118  edgssv2en  16120  uspgredg2vlem  16141  usgredg2vlem1  16143  uhgr0vsize0en  16156  wlkepvtx  16296  bj-bdfindes  16645  bj-findes  16677  2omap  16695