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  1435  exmid1stab  4296  imainss  5150  xpexr2m  5176  funeu2  5350  imadiflem  5406  fnop  5432  ssimaex  5703  isosolem  5960  acexmidlem2  6010  fnovex  6046  cnvoprab  6394  smores3  6454  freccllem  6563  riinerm  6772  pw1fin  7095  enq0sym  7642  peano5nnnn  8102  axcaucvglemres  8109  uzind3  9583  xrltnsym  10018  xsubge0  10106  0fz1  10270  seqf  10716  seq3f1oleml  10768  exp1  10797  expp1  10798  resqrexlemf1  11559  resqrexlemfp1  11560  clim2ser  11888  clim2ser2  11889  isermulc2  11891  summodclem3  11931  fisumss  11943  fsum3cvg3  11947  iserabs  12026  isumshft  12041  isumsplit  12042  geoisum1  12070  geoisum1c  12071  cvgratnnlemnexp  12075  cvgratz  12083  mertenslem2  12087  clim2prod  12090  clim2divap  12091  fprodseq  12134  prodssdc  12140  fprodssdc  12141  effsumlt  12243  efgt1p  12247  gcd0id  12540  nninfctlemfo  12601  lcmgcd  12640  lcmdvds  12641  lcmid  12642  isprm2lem  12678  pcmpt  12906  ennnfonelemjn  13013  issgrpd  13485  mulg1  13706  srglmhm  13996  srgrmhm  13997  ringlghm  14064  ringrghm  14065  neipsm  14868  xmetpsmet  15083  comet  15213  metrest  15220  expcncf  15323  lgscllem  15726  lgsdir2  15752  lgsdirnn0  15766  lgsdinn0  15767  cvgcmp2nlemabs  16572  nconstwlpolem  16605