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  4077  opabss  4148  triun  4195  poirr  4399  wepo  4451  wetrep  4452  rexxfrd  4555  reg3exmidlemwe  4672  nnsuc  4709  fnfco  5505  fun11iun  5598  fnressn  5832  fvpr1g  5852  fvtp1g  5854  fvtp3g  5856  fvtp3  5859  f1mpt  5904  caovlem2d  6207  offval  6235  dfoprab3  6346  1stconst  6378  2ndconst  6379  poxp  6389  tfrlemisucaccv  6482  tfr1onlemsucaccv  6498  tfrcllemsucaccv  6511  fiintim  7109  pr1or2  7383  addclpi  7530  addnidpig  7539  reapmul1  8758  nnnn0addcl  9415  un0addcl  9418  un0mulcl  9419  zltnle  9508  nn0ge0div  9550  uzind3  9576  uzind4  9800  ltsubrp  9903  ltaddrp  9904  xrlttr  10008  xrltso  10009  xltnegi  10048  xaddnemnf  10070  xaddnepnf  10071  xaddcom  10074  xnegdi  10081  xsubge0  10094  fzind2  10462  qltnle  10480  qbtwnxr  10494  exp3vallem  10779  expp1  10785  expnegap0  10786  expcllem  10789  mulexpzap  10818  expaddzap  10822  expmulzap  10824  hashunlem  11043  cats1un  11274  reuccatpfxs1  11300  shftf  11362  sqrtdiv  11574  mulcn2  11844  summodclem2  11914  fsum3  11919  cvgratz  12064  prodmodclem2  12109  zproddc  12111  prodsnf  12124  dvdsflip  12383  dvdsfac  12392  bitsfzolem  12486  lcmgcdlem  12620  rpexp1i  12697  hashdvds  12764  hashgcdlem  12781  phisum  12784  pcqcl  12850  pcid  12868  ssnnctlemct  13038  issubmd  13528  grpinvnzcl  13626  mulgneg  13698  mulgnn0z  13707  01eq0ring  14174  lmss  14941  xmetrtri  15071  blssioo  15248  divcnap  15260  dedekindicc  15328  dvidlemap  15386  dvidrelem  15387  dvidsslem  15388  dvrecap  15408  dveflem  15421  lgsval3  15718  lgsdir2  15733  2sqlem6  15820  umgredg  15964  umgrpredgv  15966  umgredgne  15969  umgredgnlp  15971  usgredgppren  16016  edgssv2en  16018  uspgredg2vlem  16039  usgredg2vlem1  16041  uhgr0vsize0en  16054  bj-bdfindes  16421  bj-findes  16453  2omap  16472