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  1438  exmid1stab  4321  imainss  5178  xpexr2m  5204  funeu2  5378  imadiflem  5435  fnop  5461  ssimaex  5738  isosolem  5997  acexmidlem2  6047  fnovex  6083  cnvoprab  6430  suppssdc  6460  smores3  6524  freccllem  6633  riinerm  6842  pw1fin  7170  enq0sym  7747  peano5nnnn  8207  axcaucvglemres  8214  uzind3  9691  xrltnsym  10126  xsubge0  10214  0fz1  10379  seqf  10826  seq3f1oleml  10878  exp1  10907  expp1  10908  resqrexlemf1  11693  resqrexlemfp1  11694  clim2ser  12022  clim2ser2  12023  isermulc2  12025  summodclem3  12066  fisumss  12078  fsum3cvg3  12082  iserabs  12161  isumshft  12176  isumsplit  12177  geoisum1  12205  geoisum1c  12206  cvgratnnlemnexp  12210  cvgratz  12218  mertenslem2  12222  clim2prod  12225  clim2divap  12226  fprodseq  12269  prodssdc  12275  fprodssdc  12276  effsumlt  12378  efgt1p  12382  gcd0id  12675  nninfctlemfo  12736  lcmgcd  12775  lcmdvds  12776  lcmid  12777  isprm2lem  12813  pcmpt  13041  ennnfonelemjn  13153  issgrpd  13625  mulg1  13846  srglmhm  14137  srgrmhm  14138  ringlghm  14205  ringrghm  14206  neipsm  15019  xmetpsmet  15234  comet  15364  metrest  15371  expcncf  15474  lgscllem  15880  lgsdir2  15906  lgsdirnn0  15920  lgsdinn0  15921  eupth2lem3lem7fi  16469  cvgcmp2nlemabs  16816  nconstwlpolem  16851  gfsumval  16862