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  948  bm1.1  2223  eqtr3  2258  elnelne1  2524  elnelne2  2525  morex  3010  reuss2  3513  reupick  3517  rabsneu  3783  invdisjrab  4122  opabss  4193  triun  4240  poirr  4450  wepo  4502  wetrep  4503  rexxfrd  4607  reg3exmidlemwe  4724  nnsuc  4761  fnfco  5562  fun11iun  5658  fnressn  5895  fvpr1g  5915  fvtp1g  5917  fvtp3g  5919  fvtp3  5922  f1mpt  5971  caovlem2d  6276  offval  6304  dfoprab3  6419  1stconst  6451  2ndconst  6452  poxp  6462  suppssrst  6495  suppssrgst  6496  tfrlemisucaccv  6590  tfr1onlemsucaccv  6606  tfrcllemsucaccv  6619  fiintim  7232  2omap  7312  pr1or2  7534  addclpi  7688  addnidpig  7697  reapmul1  8917  nnnn0addcl  9576  un0addcl  9579  un0mulcl  9580  zltnle  9673  nn0ge0div  9716  uzind3  9742  uzind4  9971  ltsubrp  10074  ltaddrp  10075  xrlttr  10180  xrltso  10181  xltnegi  10220  xaddnemnf  10242  xaddnepnf  10243  xaddcom  10246  xnegdi  10253  xsubge0  10266  fzind2  10641  qltnle  10661  qbtwnxr  10675  exp3vallem  10960  expp1  10966  expnegap0  10967  expcllem  10970  mulexpzap  10999  expaddzap  11003  expmulzap  11005  hashunlem  11227  cats1un  11476  reuccatpfxs1  11502  shftf  11578  sqrtdiv  11791  mulcn2  12061  summodclem2  12132  fsum3  12137  cvgratz  12282  prodmodclem2  12327  zproddc  12329  prodsnf  12342  dvdsflip  12601  dvdsfac  12610  bitsfzolem  12704  lcmgcdlem  12838  rpexp1i  12915  hashdvds  12982  hashgcdlem  12999  phisum  13002  pcqcl  13068  pcid  13086  ballotfilemfc0  13215  ballotfilemfcc  13216  ssnnctlemct  13320  issubmd  13764  grpinvnzcl  13860  mulgneg  13926  mulgnn0z  13935  01eq0ring  14479  lmss  15330  xmetrtri  15460  blssioo  15637  divcnap  15649  dedekindicc  15717  dvidlemap  15775  dvidrelem  15776  dvidsslem  15777  dvrecap  15797  dveflem  15810  pellexlem3  16076  lgsval3  16120  lgsdir2  16135  2sqlem6  16222  umgredg  16369  umgrpredgv  16371  umgredgne  16374  umgredgnlp  16376  usgredgppren  16421  edgssv2en  16423  uspgredg2vlem  16444  usgredg2vlem1  16446  uhgr0vsize0en  16459  wlkepvtx  16599  bj-bdfindes  16958  bj-findes  16990