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  5964  acexmidlem2  6014  fnovex  6050  cnvoprab  6398  smores3  6458  freccllem  6567  riinerm  6776  pw1fin  7101  enq0sym  7651  peano5nnnn  8111  axcaucvglemres  8118  uzind3  9592  xrltnsym  10027  xsubge0  10115  0fz1  10279  seqf  10725  seq3f1oleml  10777  exp1  10806  expp1  10807  resqrexlemf1  11568  resqrexlemfp1  11569  clim2ser  11897  clim2ser2  11898  isermulc2  11900  summodclem3  11940  fisumss  11952  fsum3cvg3  11956  iserabs  12035  isumshft  12050  isumsplit  12051  geoisum1  12079  geoisum1c  12080  cvgratnnlemnexp  12084  cvgratz  12092  mertenslem2  12096  clim2prod  12099  clim2divap  12100  fprodseq  12143  prodssdc  12149  fprodssdc  12150  effsumlt  12252  efgt1p  12256  gcd0id  12549  nninfctlemfo  12610  lcmgcd  12649  lcmdvds  12650  lcmid  12651  isprm2lem  12687  pcmpt  12915  ennnfonelemjn  13022  issgrpd  13494  mulg1  13715  srglmhm  14005  srgrmhm  14006  ringlghm  14073  ringrghm  14074  neipsm  14877  xmetpsmet  15092  comet  15222  metrest  15229  expcncf  15332  lgscllem  15735  lgsdir2  15761  lgsdirnn0  15775  lgsdinn0  15776  cvgcmp2nlemabs  16636  nconstwlpolem  16669  gfsumval  16680