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  7318  pr1or2  7540  addclpi  7694  addnidpig  7703  reapmul1  8924  nnnn0addcl  9595  un0addcl  9598  un0mulcl  9599  zltnle  9692  nn0ge0div  9735  uzind3  9761  uzind4  9990  ltsubrp  10093  ltaddrp  10094  xrlttr  10199  xrltso  10200  xltnegi  10239  xaddnemnf  10261  xaddnepnf  10262  xaddcom  10265  xnegdi  10272  xsubge0  10285  fzind2  10660  qltnle  10680  qbtwnxr  10694  exp3vallem  10979  expp1  10985  expnegap0  10986  expcllem  10989  mulexpzap  11018  expaddzap  11022  expmulzap  11024  hashunlem  11246  cats1un  11495  reuccatpfxs1  11521  shftf  11597  sqrtdiv  11810  mulcn2  12080  summodclem2  12151  fsum3  12156  cvgratz  12301  prodmodclem2  12346  zproddc  12348  prodsnf  12361  dvdsflip  12620  dvdsfac  12629  bitsfzolem  12723  lcmgcdlem  12857  rpexp1i  12934  hashdvds  13001  hashgcdlem  13018  phisum  13021  pcqcl  13087  pcid  13105  ballotfilemfc0  13234  ballotfilemfcc  13235  ssnnctlemct  13339  issubmd  13783  grpinvnzcl  13879  mulgneg  13945  mulgnn0z  13954  01eq0ring  14498  lmss  15349  xmetrtri  15479  blssioo  15656  divcnap  15668  dedekindicc  15736  dvidlemap  15794  dvidrelem  15795  dvidsslem  15796  dvrecap  15816  dveflem  15829  pellexlem3  16099  lgsval3  16149  lgsdir2  16164  2sqlem6  16251  umgredg  16398  umgrpredgv  16400  umgredgne  16403  umgredgnlp  16405  usgredgppren  16450  edgssv2en  16452  uspgredg2vlem  16473  usgredg2vlem1  16475  uhgr0vsize0en  16488  wlkepvtx  16628  bj-bdfindes  16987  bj-findes  17019