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  4195  triun  4242  poirr  4452  wepo  4504  wetrep  4505  rexxfrd  4609  reg3exmidlemwe  4726  nnsuc  4763  fnfco  5564  fun11iun  5660  fnressn  5901  fvpr1g  5921  fvtp1g  5923  fvtp3g  5925  fvtp3  5928  f1mpt  5977  caovlem2d  6282  offval  6310  dfoprab3  6425  1stconst  6457  2ndconst  6458  poxp  6468  suppssrst  6501  suppssrgst  6502  tfrlemisucaccv  6596  tfr1onlemsucaccv  6612  tfrcllemsucaccv  6625  fiintim  7238  2omap  7319  pr1or2  7541  addclpi  7695  addnidpig  7704  reapmul1  8926  nnnn0addcl  9598  un0addcl  9601  un0mulcl  9602  zltnle  9695  nn0ge0div  9738  uzind3  9764  uzind4  9998  ltsubrp  10102  ltaddrp  10103  xrlttr  10208  xrltso  10209  xltnegi  10248  xaddnemnf  10270  xaddnepnf  10271  xaddcom  10274  xnegdi  10281  xsubge0  10294  fzind2  10669  qltnle  10689  qbtwnxr  10703  exp3vallem  10991  expp1  10997  expnegap0  10998  expcllem  11001  mulexpzap  11030  expaddzap  11034  expmulzap  11036  hashunlem  11259  cats1un  11508  reuccatpfxs1  11534  shftf  11610  sqrtdiv  11823  mulcn2  12096  summodclem2  12167  fsum3  12172  cvgratz  12317  prodmodclem2  12362  zproddc  12364  prodsnf  12377  dvdsflip  12636  dvdsfac  12645  bitsfzolem  12739  lcmgcdlem  12873  rpexp1i  12951  hashdvds  13021  hashgcdlem  13038  phisum  13041  pcqcl  13107  pcid  13125  ballotfilemfc0  13283  ballotfilemfcc  13284  ssnnctlemct  13388  issubmd  13832  grpinvnzcl  13928  mulgneg  13994  mulgnn0z  14003  01eq0ring  14547  psrbaglefifi  15114  lmss  15399  xmetrtri  15529  blssioo  15706  divcnap  15718  dedekindicc  15786  dvidlemap  15844  dvidrelem  15845  dvidsslem  15846  dvrecap  15866  dveflem  15879  pellexlem3  16153  prmorcht  16204  lgsval3  16259  lgsdir2  16274  2sqlem6  16361  umgredg  16508  umgrpredgv  16510  umgredgne  16513  umgredgnlp  16515  usgredgppren  16560  edgssv2en  16562  uspgredg2vlem  16583  usgredg2vlem1  16585  uhgr0vsize0en  16598  wlkepvtx  16738  bj-bdfindes  17097  bj-findes  17129