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  4292  imainss  5144  xpexr2m  5170  funeu2  5344  imadiflem  5400  fnop  5426  ssimaex  5697  isosolem  5954  acexmidlem2  6004  fnovex  6040  cnvoprab  6386  smores3  6445  freccllem  6554  riinerm  6763  pw1fin  7083  enq0sym  7630  peano5nnnn  8090  axcaucvglemres  8097  uzind3  9571  xrltnsym  10001  xsubge0  10089  0fz1  10253  seqf  10698  seq3f1oleml  10750  exp1  10779  expp1  10780  resqrexlemf1  11534  resqrexlemfp1  11535  clim2ser  11863  clim2ser2  11864  isermulc2  11866  summodclem3  11906  fisumss  11918  fsum3cvg3  11922  iserabs  12001  isumshft  12016  isumsplit  12017  geoisum1  12045  geoisum1c  12046  cvgratnnlemnexp  12050  cvgratz  12058  mertenslem2  12062  clim2prod  12065  clim2divap  12066  fprodseq  12109  prodssdc  12115  fprodssdc  12116  effsumlt  12218  efgt1p  12222  gcd0id  12515  nninfctlemfo  12576  lcmgcd  12615  lcmdvds  12616  lcmid  12617  isprm2lem  12653  pcmpt  12881  ennnfonelemjn  12988  issgrpd  13460  mulg1  13681  srglmhm  13971  srgrmhm  13972  ringlghm  14039  ringrghm  14040  neipsm  14843  xmetpsmet  15058  comet  15188  metrest  15195  expcncf  15298  lgscllem  15701  lgsdir2  15727  lgsdirnn0  15741  lgsdinn0  15742  cvgcmp2nlemabs  16460  nconstwlpolem  16493