Theorem sylan2b 285

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 119	. 2 ⊢ (𝜑 → 𝜒)
3		sylan2b.2	. 2 ⊢ ((𝜓 ∧ 𝜒) → 𝜃)
4	2, 3	sylan2 284	1 ⊢ ((𝜓 ∧ 𝜑) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 103   ↔ wb 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  syl2anb  289  dcor  919  bm1.1  2124  eqtr3  2159  elnelne1  2412  elnelne2  2413  morex  2868  reuss2  3356  reupick  3360  rabsneu  3596  opabss  3992  triun  4039  poirr  4229  wepo  4281  wetrep  4282  rexxfrd  4384  reg3exmidlemwe  4493  nnsuc  4529  fnfco  5297  fun11iun  5388  fnressn  5606  fvpr1g  5626  fvtp1g  5628  fvtp3g  5630  fvtp3  5633  f1mpt  5672  caovlem2d  5963  offval  5989  dfoprab3  6089  1stconst  6118  2ndconst  6119  poxp  6129  tfrlemisucaccv  6222  tfr1onlemsucaccv  6238  tfrcllemsucaccv  6251  fiintim  6817  addclpi  7135  addnidpig  7144  reapmul1  8357  nnnn0addcl  9007  un0addcl  9010  un0mulcl  9011  zltnle  9100  nn0ge0div  9138  uzind3  9164  uzind4  9383  ltsubrp  9478  ltaddrp  9479  xrlttr  9581  xrltso  9582  xltnegi  9618  xaddnemnf  9640  xaddnepnf  9641  xaddcom  9644  xnegdi  9651  xsubge0  9664  fzind2  10016  qltnle  10023  qbtwnxr  10035  exp3vallem  10294  expp1  10300  expnegap0  10301  expcllem  10304  mulexpzap  10333  expaddzap  10337  expmulzap  10339  hashunlem  10550  shftf  10602  sqrtdiv  10814  mulcn2  11081  summodclem2  11151  fsum3  11156  cvgratz  11301  prodmodclem2  11346  dvdsflip  11549  dvdsfac  11558  lcmgcdlem  11758  rpexp1i  11832  hashdvds  11897  hashgcdlem  11903  lmss  12415  xmetrtri  12545  blssioo  12714  divcnap  12724  dedekindicc  12780  dvidlemap  12829  dvrecap  12846  dveflem  12855  bj-bdfindes  13147  bj-findes  13179