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  941  bm1.1  2214  eqtr3  2249  elnelne1  2504  elnelne2  2505  morex  2987  reuss2  3484  reupick  3488  rabsneu  3739  invdisjrab  4076  opabss  4147  triun  4194  poirr  4395  wepo  4447  wetrep  4448  rexxfrd  4551  reg3exmidlemwe  4668  nnsuc  4705  fnfco  5496  fun11iun  5589  fnressn  5818  fvpr1g  5838  fvtp1g  5840  fvtp3g  5842  fvtp3  5845  f1mpt  5888  caovlem2d  6189  offval  6216  dfoprab3  6327  1stconst  6357  2ndconst  6358  poxp  6368  tfrlemisucaccv  6461  tfr1onlemsucaccv  6477  tfrcllemsucaccv  6490  fiintim  7081  pr1or2  7355  addclpi  7502  addnidpig  7511  reapmul1  8730  nnnn0addcl  9387  un0addcl  9390  un0mulcl  9391  zltnle  9480  nn0ge0div  9522  uzind3  9548  uzind4  9771  ltsubrp  9874  ltaddrp  9875  xrlttr  9979  xrltso  9980  xltnegi  10019  xaddnemnf  10041  xaddnepnf  10042  xaddcom  10045  xnegdi  10052  xsubge0  10065  fzind2  10432  qltnle  10450  qbtwnxr  10464  exp3vallem  10749  expp1  10755  expnegap0  10756  expcllem  10759  mulexpzap  10788  expaddzap  10792  expmulzap  10794  hashunlem  11013  cats1un  11239  reuccatpfxs1  11265  shftf  11327  sqrtdiv  11539  mulcn2  11809  summodclem2  11879  fsum3  11884  cvgratz  12029  prodmodclem2  12074  zproddc  12076  prodsnf  12089  dvdsflip  12348  dvdsfac  12357  bitsfzolem  12451  lcmgcdlem  12585  rpexp1i  12662  hashdvds  12729  hashgcdlem  12746  phisum  12749  pcqcl  12815  pcid  12833  ssnnctlemct  13003  issubmd  13493  grpinvnzcl  13591  mulgneg  13663  mulgnn0z  13672  01eq0ring  14138  lmss  14905  xmetrtri  15035  blssioo  15212  divcnap  15224  dedekindicc  15292  dvidlemap  15350  dvidrelem  15351  dvidsslem  15352  dvrecap  15372  dveflem  15385  lgsval3  15682  lgsdir2  15697  2sqlem6  15784  umgredg  15928  umgrpredgv  15930  umgredgne  15933  umgredgnlp  15935  usgredgppren  15980  edgssv2en  15982  uspgredg2vlem  16003  usgredg2vlem1  16005  bj-bdfindes  16242  bj-findes  16274  2omap  16290