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  2988  reuss2  3485  reupick  3489  rabsneu  3742  invdisjrab  4080  opabss  4151  triun  4198  poirr  4402  wepo  4454  wetrep  4455  rexxfrd  4558  reg3exmidlemwe  4675  nnsuc  4712  fnfco  5508  fun11iun  5601  fnressn  5835  fvpr1g  5855  fvtp1g  5857  fvtp3g  5859  fvtp3  5862  f1mpt  5907  caovlem2d  6210  offval  6238  dfoprab3  6349  1stconst  6381  2ndconst  6382  poxp  6392  tfrlemisucaccv  6486  tfr1onlemsucaccv  6502  tfrcllemsucaccv  6515  fiintim  7118  pr1or2  7393  addclpi  7540  addnidpig  7549  reapmul1  8768  nnnn0addcl  9425  un0addcl  9428  un0mulcl  9429  zltnle  9518  nn0ge0div  9560  uzind3  9586  uzind4  9815  ltsubrp  9918  ltaddrp  9919  xrlttr  10023  xrltso  10024  xltnegi  10063  xaddnemnf  10085  xaddnepnf  10086  xaddcom  10089  xnegdi  10096  xsubge0  10109  fzind2  10478  qltnle  10496  qbtwnxr  10510  exp3vallem  10795  expp1  10801  expnegap0  10802  expcllem  10805  mulexpzap  10834  expaddzap  10838  expmulzap  10840  hashunlem  11060  cats1un  11295  reuccatpfxs1  11321  shftf  11384  sqrtdiv  11596  mulcn2  11866  summodclem2  11936  fsum3  11941  cvgratz  12086  prodmodclem2  12131  zproddc  12133  prodsnf  12146  dvdsflip  12405  dvdsfac  12414  bitsfzolem  12508  lcmgcdlem  12642  rpexp1i  12719  hashdvds  12786  hashgcdlem  12803  phisum  12806  pcqcl  12872  pcid  12890  ssnnctlemct  13060  issubmd  13550  grpinvnzcl  13648  mulgneg  13720  mulgnn0z  13729  01eq0ring  14196  lmss  14963  xmetrtri  15093  blssioo  15270  divcnap  15282  dedekindicc  15350  dvidlemap  15408  dvidrelem  15409  dvidsslem  15410  dvrecap  15430  dveflem  15443  lgsval3  15740  lgsdir2  15755  2sqlem6  15842  umgredg  15989  umgrpredgv  15991  umgredgne  15994  umgredgnlp  15996  usgredgppren  16041  edgssv2en  16043  uspgredg2vlem  16064  usgredg2vlem1  16066  uhgr0vsize0en  16079  bj-bdfindes  16494  bj-findes  16526  2omap  16544