Theorem sylan2br 288

Description: A syllogism inference. (Contributed by NM, 21-Apr-1994.)

Hypotheses

Ref	Expression
sylan2br.1	⊢ (𝜒 ↔ 𝜑)
sylan2br.2	⊢ ((𝜓 ∧ 𝜒) → 𝜃)

Assertion

Ref	Expression
sylan2br	⊢ ((𝜓 ∧ 𝜑) → 𝜃)

Proof of Theorem sylan2br

Step	Hyp	Ref	Expression
1		sylan2br.1	. . 3 ⊢ (𝜒 ↔ 𝜑)
2	1	biimpri 133	. 2 ⊢ (𝜑 → 𝜒)
3		sylan2br.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:  syl2anbr  292  xordc1  1438  exmid1stab  4304  imainss  5159  xpexr2m  5185  funeu2  5359  imadiflem  5416  fnop  5442  ssimaex  5716  isosolem  5975  acexmidlem2  6025  fnovex  6061  cnvoprab  6408  suppssdc  6438  smores3  6502  freccllem  6611  riinerm  6820  pw1fin  7145  enq0sym  7695  peano5nnnn  8155  axcaucvglemres  8162  uzind3  9637  xrltnsym  10072  xsubge0  10160  0fz1  10325  seqf  10772  seq3f1oleml  10824  exp1  10853  expp1  10854  resqrexlemf1  11631  resqrexlemfp1  11632  clim2ser  11960  clim2ser2  11961  isermulc2  11963  summodclem3  12004  fisumss  12016  fsum3cvg3  12020  iserabs  12099  isumshft  12114  isumsplit  12115  geoisum1  12143  geoisum1c  12144  cvgratnnlemnexp  12148  cvgratz  12156  mertenslem2  12160  clim2prod  12163  clim2divap  12164  fprodseq  12207  prodssdc  12213  fprodssdc  12214  effsumlt  12316  efgt1p  12320  gcd0id  12613  nninfctlemfo  12674  lcmgcd  12713  lcmdvds  12714  lcmid  12715  isprm2lem  12751  pcmpt  12979  ennnfonelemjn  13086  issgrpd  13558  mulg1  13779  srglmhm  14070  srgrmhm  14071  ringlghm  14138  ringrghm  14139  neipsm  14948  xmetpsmet  15163  comet  15293  metrest  15300  expcncf  15403  lgscllem  15809  lgsdir2  15835  lgsdirnn0  15849  lgsdinn0  15850  eupth2lem3lem7fi  16398  cvgcmp2nlemabs  16747  nconstwlpolem  16781  gfsumval  16792