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  935  bm1.1  2162  eqtr3  2197  elnelne1  2451  elnelne2  2452  morex  2921  reuss2  3415  reupick  3419  rabsneu  3665  opabss  4067  triun  4114  poirr  4307  wepo  4359  wetrep  4360  rexxfrd  4463  reg3exmidlemwe  4578  nnsuc  4615  fnfco  5390  fun11iun  5482  fnressn  5702  fvpr1g  5722  fvtp1g  5724  fvtp3g  5726  fvtp3  5729  f1mpt  5771  caovlem2d  6066  offval  6089  dfoprab3  6191  1stconst  6221  2ndconst  6222  poxp  6232  tfrlemisucaccv  6325  tfr1onlemsucaccv  6341  tfrcllemsucaccv  6354  fiintim  6927  addclpi  7325  addnidpig  7334  reapmul1  8551  nnnn0addcl  9205  un0addcl  9208  un0mulcl  9209  zltnle  9298  nn0ge0div  9339  uzind3  9365  uzind4  9587  ltsubrp  9689  ltaddrp  9690  xrlttr  9794  xrltso  9795  xltnegi  9834  xaddnemnf  9856  xaddnepnf  9857  xaddcom  9860  xnegdi  9867  xsubge0  9880  fzind2  10238  qltnle  10245  qbtwnxr  10257  exp3vallem  10520  expp1  10526  expnegap0  10527  expcllem  10530  mulexpzap  10559  expaddzap  10563  expmulzap  10565  hashunlem  10783  shftf  10838  sqrtdiv  11050  mulcn2  11319  summodclem2  11389  fsum3  11394  cvgratz  11539  prodmodclem2  11584  zproddc  11586  prodsnf  11599  dvdsflip  11856  dvdsfac  11865  lcmgcdlem  12076  rpexp1i  12153  hashdvds  12220  hashgcdlem  12237  phisum  12239  pcqcl  12305  pcid  12322  ssnnctlemct  12446  issubmd  12864  grpinvnzcl  12941  mulgneg  13000  mulgnn0z  13008  01eq0ring  13328  lmss  13716  xmetrtri  13846  blssioo  14015  divcnap  14025  dedekindicc  14081  dvidlemap  14130  dvrecap  14147  dveflem  14157  lgsval3  14389  lgsdir2  14404  2sqlem6  14437  bj-bdfindes  14671  bj-findes  14703