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  943  bm1.1  2216  eqtr3  2251  elnelne1  2506  elnelne2  2507  morex  2990  reuss2  3487  reupick  3491  rabsneu  3744  invdisjrab  4082  opabss  4153  triun  4200  poirr  4404  wepo  4456  wetrep  4457  rexxfrd  4560  reg3exmidlemwe  4677  nnsuc  4714  fnfco  5511  fun11iun  5604  fnressn  5840  fvpr1g  5860  fvtp1g  5862  fvtp3g  5864  fvtp3  5867  f1mpt  5912  caovlem2d  6215  offval  6243  dfoprab3  6354  1stconst  6386  2ndconst  6387  poxp  6397  tfrlemisucaccv  6491  tfr1onlemsucaccv  6507  tfrcllemsucaccv  6520  fiintim  7123  pr1or2  7399  addclpi  7547  addnidpig  7556  reapmul1  8775  nnnn0addcl  9432  un0addcl  9435  un0mulcl  9436  zltnle  9525  nn0ge0div  9567  uzind3  9593  uzind4  9822  ltsubrp  9925  ltaddrp  9926  xrlttr  10030  xrltso  10031  xltnegi  10070  xaddnemnf  10092  xaddnepnf  10093  xaddcom  10096  xnegdi  10103  xsubge0  10116  fzind2  10486  qltnle  10504  qbtwnxr  10518  exp3vallem  10803  expp1  10809  expnegap0  10810  expcllem  10813  mulexpzap  10842  expaddzap  10846  expmulzap  10848  hashunlem  11068  cats1un  11306  reuccatpfxs1  11332  shftf  11395  sqrtdiv  11607  mulcn2  11877  summodclem2  11948  fsum3  11953  cvgratz  12098  prodmodclem2  12143  zproddc  12145  prodsnf  12158  dvdsflip  12417  dvdsfac  12426  bitsfzolem  12520  lcmgcdlem  12654  rpexp1i  12731  hashdvds  12798  hashgcdlem  12815  phisum  12818  pcqcl  12884  pcid  12902  ssnnctlemct  13072  issubmd  13562  grpinvnzcl  13660  mulgneg  13732  mulgnn0z  13741  01eq0ring  14209  lmss  14976  xmetrtri  15106  blssioo  15283  divcnap  15295  dedekindicc  15363  dvidlemap  15421  dvidrelem  15422  dvidsslem  15423  dvrecap  15443  dveflem  15456  lgsval3  15753  lgsdir2  15768  2sqlem6  15855  umgredg  16002  umgrpredgv  16004  umgredgne  16007  umgredgnlp  16009  usgredgppren  16054  edgssv2en  16056  uspgredg2vlem  16077  usgredg2vlem1  16079  uhgr0vsize0en  16092  wlkepvtx  16232  bj-bdfindes  16570  bj-findes  16602  2omap  16620