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  4268  imainss  5117  xpexr2m  5143  funeu2  5316  imadiflem  5372  fnop  5398  ssimaex  5663  isosolem  5916  acexmidlem2  5964  fnovex  6000  cnvoprab  6343  smores3  6402  freccllem  6511  riinerm  6718  pw1fin  7033  enq0sym  7580  peano5nnnn  8040  axcaucvglemres  8047  uzind3  9521  xrltnsym  9950  xsubge0  10038  0fz1  10202  seqf  10646  seq3f1oleml  10698  exp1  10727  expp1  10728  resqrexlemf1  11434  resqrexlemfp1  11435  clim2ser  11763  clim2ser2  11764  isermulc2  11766  summodclem3  11806  fisumss  11818  fsum3cvg3  11822  iserabs  11901  isumshft  11916  isumsplit  11917  geoisum1  11945  geoisum1c  11946  cvgratnnlemnexp  11950  cvgratz  11958  mertenslem2  11962  clim2prod  11965  clim2divap  11966  fprodseq  12009  prodssdc  12015  fprodssdc  12016  effsumlt  12118  efgt1p  12122  gcd0id  12415  nninfctlemfo  12476  lcmgcd  12515  lcmdvds  12516  lcmid  12517  isprm2lem  12553  pcmpt  12781  ennnfonelemjn  12888  issgrpd  13359  mulg1  13580  srglmhm  13870  srgrmhm  13871  ringlghm  13938  ringrghm  13939  neipsm  14741  xmetpsmet  14956  comet  15086  metrest  15093  expcncf  15196  lgscllem  15599  lgsdir2  15625  lgsdirnn0  15639  lgsdinn0  15640  cvgcmp2nlemabs  16173  nconstwlpolem  16206