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  2219  eqtr3  2254  elnelne1  2518  elnelne2  2519  morex  3004  reuss2  3505  reupick  3509  rabsneu  3769  invdisjrab  4108  opabss  4179  triun  4226  poirr  4433  wepo  4485  wetrep  4486  rexxfrd  4589  reg3exmidlemwe  4706  nnsuc  4743  fnfco  5544  fun11iun  5640  fnressn  5875  fvpr1g  5895  fvtp1g  5897  fvtp3g  5899  fvtp3  5902  f1mpt  5950  caovlem2d  6255  offval  6283  dfoprab3  6398  1stconst  6430  2ndconst  6431  poxp  6441  suppssrst  6474  suppssrgst  6475  tfrlemisucaccv  6569  tfr1onlemsucaccv  6585  tfrcllemsucaccv  6598  fiintim  7204  2omap  7282  pr1or2  7504  addclpi  7658  addnidpig  7667  reapmul1  8887  nnnn0addcl  9546  un0addcl  9549  un0mulcl  9550  zltnle  9643  nn0ge0div  9686  uzind3  9712  uzind4  9941  ltsubrp  10044  ltaddrp  10045  xrlttr  10150  xrltso  10151  xltnegi  10190  xaddnemnf  10212  xaddnepnf  10213  xaddcom  10216  xnegdi  10223  xsubge0  10236  fzind2  10610  qltnle  10630  qbtwnxr  10644  exp3vallem  10929  expp1  10935  expnegap0  10936  expcllem  10939  mulexpzap  10968  expaddzap  10972  expmulzap  10974  hashunlem  11196  cats1un  11441  reuccatpfxs1  11467  shftf  11543  sqrtdiv  11756  mulcn2  12026  summodclem2  12097  fsum3  12102  cvgratz  12247  prodmodclem2  12292  zproddc  12294  prodsnf  12307  dvdsflip  12566  dvdsfac  12575  bitsfzolem  12669  lcmgcdlem  12803  rpexp1i  12880  hashdvds  12947  hashgcdlem  12964  phisum  12967  pcqcl  13033  pcid  13051  ballotfilemfc0  13180  ballotfilemfcc  13181  ssnnctlemct  13285  issubmd  13733  grpinvnzcl  13831  mulgneg  13897  mulgnn0z  13906  01eq0ring  14438  lmss  15241  xmetrtri  15371  blssioo  15548  divcnap  15560  dedekindicc  15628  dvidlemap  15686  dvidrelem  15687  dvidsslem  15688  dvrecap  15708  dveflem  15721  pellexlem3  15977  lgsval3  16021  lgsdir2  16036  2sqlem6  16123  umgredg  16270  umgrpredgv  16272  umgredgne  16275  umgredgnlp  16277  usgredgppren  16322  edgssv2en  16324  uspgredg2vlem  16345  usgredg2vlem1  16347  uhgr0vsize0en  16360  wlkepvtx  16500  bj-bdfindes  16859  bj-findes  16891