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  1437  exmid1stab  4298  imainss  5152  xpexr2m  5178  funeu2  5352  imadiflem  5409  fnop  5435  ssimaex  5707  isosolem  5965  acexmidlem2  6015  fnovex  6051  cnvoprab  6399  smores3  6459  freccllem  6568  riinerm  6777  pw1fin  7102  enq0sym  7652  peano5nnnn  8112  axcaucvglemres  8119  uzind3  9593  xrltnsym  10028  xsubge0  10116  0fz1  10280  seqf  10727  seq3f1oleml  10779  exp1  10808  expp1  10809  resqrexlemf1  11573  resqrexlemfp1  11574  clim2ser  11902  clim2ser2  11903  isermulc2  11905  summodclem3  11946  fisumss  11958  fsum3cvg3  11962  iserabs  12041  isumshft  12056  isumsplit  12057  geoisum1  12085  geoisum1c  12086  cvgratnnlemnexp  12090  cvgratz  12098  mertenslem2  12102  clim2prod  12105  clim2divap  12106  fprodseq  12149  prodssdc  12155  fprodssdc  12156  effsumlt  12258  efgt1p  12262  gcd0id  12555  nninfctlemfo  12616  lcmgcd  12655  lcmdvds  12656  lcmid  12657  isprm2lem  12693  pcmpt  12921  ennnfonelemjn  13028  issgrpd  13500  mulg1  13721  srglmhm  14012  srgrmhm  14013  ringlghm  14080  ringrghm  14081  neipsm  14884  xmetpsmet  15099  comet  15229  metrest  15236  expcncf  15339  lgscllem  15742  lgsdir2  15768  lgsdirnn0  15782  lgsdinn0  15783  eupth2lem3lem7fi  16331  cvgcmp2nlemabs  16662  nconstwlpolem  16696  gfsumval  16707