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  1393  exmid1stab  4210  imainss  5046  xpexr2m  5072  funeu2  5244  imadiflem  5297  fnop  5321  ssimaex  5579  isosolem  5827  acexmidlem2  5874  fnovex  5910  cnvoprab  6237  smores3  6296  freccllem  6405  riinerm  6610  pw1fin  6912  enq0sym  7433  peano5nnnn  7893  axcaucvglemres  7900  uzind3  9368  xrltnsym  9795  xsubge0  9883  0fz1  10047  seqf  10463  seq3f1oleml  10505  exp1  10528  expp1  10529  resqrexlemf1  11019  resqrexlemfp1  11020  clim2ser  11347  clim2ser2  11348  isermulc2  11350  summodclem3  11390  fisumss  11402  fsum3cvg3  11406  iserabs  11485  isumshft  11500  isumsplit  11501  geoisum1  11529  geoisum1c  11530  cvgratnnlemnexp  11534  cvgratz  11542  mertenslem2  11546  clim2prod  11549  clim2divap  11550  fprodseq  11593  prodssdc  11599  fprodssdc  11600  effsumlt  11702  efgt1p  11706  gcd0id  11982  lcmgcd  12080  lcmdvds  12081  lcmid  12082  isprm2lem  12118  pcmpt  12343  ennnfonelemjn  12405  mulg1  12995  srglmhm  13181  srgrmhm  13182  neipsm  13739  xmetpsmet  13954  comet  14084  metrest  14091  expcncf  14177  lgscllem  14493  lgsdir2  14519  lgsdirnn0  14533  lgsdinn0  14534  cvgcmp2nlemabs  14865  nconstwlpolem  14898