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  1393  imainss  5036  xpexr2m  5062  funeu2  5234  imadiflem  5287  fnop  5311  ssimaex  5569  isosolem  5815  acexmidlem2  5862  fnovex  5898  cnvoprab  6225  smores3  6284  freccllem  6393  riinerm  6598  pw1fin  6900  enq0sym  7406  peano5nnnn  7866  axcaucvglemres  7873  uzind3  9339  xrltnsym  9764  xsubge0  9852  0fz1  10015  seqf  10431  seq3f1oleml  10473  exp1  10496  expp1  10497  resqrexlemf1  10985  resqrexlemfp1  10986  clim2ser  11313  clim2ser2  11314  isermulc2  11316  summodclem3  11356  fisumss  11368  fsum3cvg3  11372  iserabs  11451  isumshft  11466  isumsplit  11467  geoisum1  11495  geoisum1c  11496  cvgratnnlemnexp  11500  cvgratz  11508  mertenslem2  11512  clim2prod  11515  clim2divap  11516  fprodseq  11559  prodssdc  11565  fprodssdc  11566  effsumlt  11668  efgt1p  11672  gcd0id  11947  lcmgcd  12045  lcmdvds  12046  lcmid  12047  isprm2lem  12083  pcmpt  12308  ennnfonelemjn  12370  mulg1  12851  srglmhm  12973  srgrmhm  12974  neipsm  13225  xmetpsmet  13440  comet  13570  metrest  13577  expcncf  13663  lgscllem  13979  lgsdir2  14005  lgsdirnn0  14019  lgsdinn0  14020  exmid1stab  14310  cvgcmp2nlemabs  14341  nconstwlpolem  14373