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  2217  eqtr3  2252  elnelne1  2516  elnelne2  2517  morex  3000  reuss2  3500  reupick  3504  rabsneu  3763  invdisjrab  4102  opabss  4173  triun  4220  poirr  4427  wepo  4479  wetrep  4480  rexxfrd  4583  reg3exmidlemwe  4700  nnsuc  4737  fnfco  5538  fun11iun  5634  fnressn  5869  fvpr1g  5889  fvtp1g  5891  fvtp3g  5893  fvtp3  5896  f1mpt  5943  caovlem2d  6246  offval  6273  dfoprab3  6384  1stconst  6416  2ndconst  6417  poxp  6427  suppssrst  6460  suppssrgst  6461  tfrlemisucaccv  6555  tfr1onlemsucaccv  6571  tfrcllemsucaccv  6584  fiintim  7190  2omap  7268  pr1or2  7490  addclpi  7641  addnidpig  7650  reapmul1  8868  nnnn0addcl  9525  un0addcl  9528  un0mulcl  9529  zltnle  9622  nn0ge0div  9664  uzind3  9690  uzind4  9919  ltsubrp  10022  ltaddrp  10023  xrlttr  10127  xrltso  10128  xltnegi  10167  xaddnemnf  10189  xaddnepnf  10190  xaddcom  10193  xnegdi  10200  xsubge0  10213  fzind2  10584  qltnle  10602  qbtwnxr  10616  exp3vallem  10901  expp1  10907  expnegap0  10908  expcllem  10911  mulexpzap  10940  expaddzap  10944  expmulzap  10946  hashunlem  11166  cats1un  11409  reuccatpfxs1  11435  shftf  11511  sqrtdiv  11723  mulcn2  11993  summodclem2  12064  fsum3  12069  cvgratz  12214  prodmodclem2  12259  zproddc  12261  prodsnf  12274  dvdsflip  12533  dvdsfac  12542  bitsfzolem  12636  lcmgcdlem  12770  rpexp1i  12847  hashdvds  12914  hashgcdlem  12931  phisum  12934  pcqcl  13000  pcid  13018  ssnnctlemct  13189  issubmd  13679  grpinvnzcl  13777  mulgneg  13849  mulgnn0z  13858  01eq0ring  14326  lmss  15103  xmetrtri  15233  blssioo  15410  divcnap  15422  dedekindicc  15490  dvidlemap  15548  dvidrelem  15549  dvidsslem  15550  dvrecap  15570  dveflem  15583  pellexlem3  15839  lgsval3  15883  lgsdir2  15898  2sqlem6  15985  umgredg  16132  umgrpredgv  16134  umgredgne  16137  umgredgnlp  16139  usgredgppren  16184  edgssv2en  16186  uspgredg2vlem  16207  usgredg2vlem1  16209  uhgr0vsize0en  16222  wlkepvtx  16362  bj-bdfindes  16711  bj-findes  16743