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  1404  exmid1stab  4241  imainss  5085  xpexr2m  5111  funeu2  5284  imadiflem  5337  fnop  5361  ssimaex  5622  isosolem  5871  acexmidlem2  5919  fnovex  5955  cnvoprab  6292  smores3  6351  freccllem  6460  riinerm  6667  pw1fin  6971  enq0sym  7499  peano5nnnn  7959  axcaucvglemres  7966  uzind3  9439  xrltnsym  9868  xsubge0  9956  0fz1  10120  seqf  10556  seq3f1oleml  10608  exp1  10637  expp1  10638  resqrexlemf1  11173  resqrexlemfp1  11174  clim2ser  11502  clim2ser2  11503  isermulc2  11505  summodclem3  11545  fisumss  11557  fsum3cvg3  11561  iserabs  11640  isumshft  11655  isumsplit  11656  geoisum1  11684  geoisum1c  11685  cvgratnnlemnexp  11689  cvgratz  11697  mertenslem2  11701  clim2prod  11704  clim2divap  11705  fprodseq  11748  prodssdc  11754  fprodssdc  11755  effsumlt  11857  efgt1p  11861  gcd0id  12146  nninfctlemfo  12207  lcmgcd  12246  lcmdvds  12247  lcmid  12248  isprm2lem  12284  pcmpt  12512  ennnfonelemjn  12619  issgrpd  13055  mulg1  13259  srglmhm  13549  srgrmhm  13550  ringlghm  13617  ringrghm  13618  neipsm  14390  xmetpsmet  14605  comet  14735  metrest  14742  expcncf  14845  lgscllem  15248  lgsdir2  15274  lgsdirnn0  15288  lgsdinn0  15289  cvgcmp2nlemabs  15676  nconstwlpolem  15709