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  4398  wepo  4450  wetrep  4451  rexxfrd  4554  reg3exmidlemwe  4671  nnsuc  4708  fnfco  5502  fun11iun  5595  fnressn  5829  fvpr1g  5849  fvtp1g  5851  fvtp3g  5853  fvtp3  5856  f1mpt  5901  caovlem2d  6204  offval  6232  dfoprab3  6343  1stconst  6373  2ndconst  6374  poxp  6384  tfrlemisucaccv  6477  tfr1onlemsucaccv  6493  tfrcllemsucaccv  6506  fiintim  7101  pr1or2  7375  addclpi  7522  addnidpig  7531  reapmul1  8750  nnnn0addcl  9407  un0addcl  9410  un0mulcl  9411  zltnle  9500  nn0ge0div  9542  uzind3  9568  uzind4  9791  ltsubrp  9894  ltaddrp  9895  xrlttr  9999  xrltso  10000  xltnegi  10039  xaddnemnf  10061  xaddnepnf  10062  xaddcom  10065  xnegdi  10072  xsubge0  10085  fzind2  10453  qltnle  10471  qbtwnxr  10485  exp3vallem  10770  expp1  10776  expnegap0  10777  expcllem  10780  mulexpzap  10809  expaddzap  10813  expmulzap  10815  hashunlem  11034  cats1un  11261  reuccatpfxs1  11287  shftf  11349  sqrtdiv  11561  mulcn2  11831  summodclem2  11901  fsum3  11906  cvgratz  12051  prodmodclem2  12096  zproddc  12098  prodsnf  12111  dvdsflip  12370  dvdsfac  12379  bitsfzolem  12473  lcmgcdlem  12607  rpexp1i  12684  hashdvds  12751  hashgcdlem  12768  phisum  12771  pcqcl  12837  pcid  12855  ssnnctlemct  13025  issubmd  13515  grpinvnzcl  13613  mulgneg  13685  mulgnn0z  13694  01eq0ring  14161  lmss  14928  xmetrtri  15058  blssioo  15235  divcnap  15247  dedekindicc  15315  dvidlemap  15373  dvidrelem  15374  dvidsslem  15375  dvrecap  15395  dveflem  15408  lgsval3  15705  lgsdir2  15720  2sqlem6  15807  umgredg  15951  umgrpredgv  15953  umgredgne  15956  umgredgnlp  15958  usgredgppren  16003  edgssv2en  16005  uspgredg2vlem  16026  usgredg2vlem1  16028  bj-bdfindes  16336  bj-findes  16368  2omap  16388