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  1413  exmid1stab  4269  imainss  5118  xpexr2m  5144  funeu2  5317  imadiflem  5373  fnop  5399  ssimaex  5665  isosolem  5918  acexmidlem2  5966  fnovex  6002  cnvoprab  6345  smores3  6404  freccllem  6513  riinerm  6720  pw1fin  7035  enq0sym  7582  peano5nnnn  8042  axcaucvglemres  8049  uzind3  9523  xrltnsym  9952  xsubge0  10040  0fz1  10204  seqf  10648  seq3f1oleml  10700  exp1  10729  expp1  10730  resqrexlemf1  11480  resqrexlemfp1  11481  clim2ser  11809  clim2ser2  11810  isermulc2  11812  summodclem3  11852  fisumss  11864  fsum3cvg3  11868  iserabs  11947  isumshft  11962  isumsplit  11963  geoisum1  11991  geoisum1c  11992  cvgratnnlemnexp  11996  cvgratz  12004  mertenslem2  12008  clim2prod  12011  clim2divap  12012  fprodseq  12055  prodssdc  12061  fprodssdc  12062  effsumlt  12164  efgt1p  12168  gcd0id  12461  nninfctlemfo  12522  lcmgcd  12561  lcmdvds  12562  lcmid  12563  isprm2lem  12599  pcmpt  12827  ennnfonelemjn  12934  issgrpd  13405  mulg1  13626  srglmhm  13916  srgrmhm  13917  ringlghm  13984  ringrghm  13985  neipsm  14787  xmetpsmet  15002  comet  15132  metrest  15139  expcncf  15242  lgscllem  15645  lgsdir2  15671  lgsdirnn0  15685  lgsdinn0  15686  cvgcmp2nlemabs  16281  nconstwlpolem  16314