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 ⊢ ((𝜓 ∧ 𝜑) → 𝜃)

This proof depends on syntax axioms:   → wi 4   ∧ wa 104   ↔ wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  syl2anbr  292  xordc1  1442  exmid1stab  4345  imainss  5203  xpexr2m  5229  funeu2  5403  imadiflem  5460  fnop  5486  ssimaex  5764  isosolem  6030  acexmidlem2  6082  fnovex  6118  cnvoprab  6470  suppssdc  6500  smores3  6564  freccllem  6673  riinerm  6882  pw1fin  7217  enq0sym  7799  peano5nnnn  8259  axcaucvglemres  8266  uzind3  9759  xrltnsym  10195  xsubge0  10283  0fz1  10449  seqf  10901  seq3f1oleml  10953  exp1  10982  expp1  10983  resqrexlemf1  11774  resqrexlemfp1  11775  clim2ser  12103  clim2ser2  12104  isermulc2  12106  summodclem3  12147  fisumss  12159  fsum3cvg3  12163  iserabs  12242  isumshft  12257  isumsplit  12258  geoisum1  12286  geoisum1c  12287  cvgratnnlemnexp  12291  cvgratz  12299  mertenslem2  12303  clim2prod  12306  clim2divap  12307  fprodseq  12350  prodssdc  12356  fprodssdc  12357  effsumlt  12459  efgt1p  12463  gcd0id  12756  nninfctlemfo  12817  lcmgcd  12856  lcmdvds  12857  lcmid  12858  isprm2lem  12894  pcmpt  13122  ballotfilemfc0  13232  ballotfilemfcc  13233  ballotfilemimin  13249  ballotfilemfrcn0  13273  ennnfonelemjn  13293  issgrpd  13727  mulg1  13932  gsumvalfi  14152  srglmhm  14297  srgrmhm  14298  ringlghm  14366  ringrghm  14367  neipsm  15255  xmetpsmet  15470  comet  15600  metrest  15607  expcncf  15710  lgscllem  16126  lgsdir2  16152  lgsdirnn0  16166  lgsdinn0  16167  eupth2lem3lem7fi  16715  cvgcmp2nlemabs  17081  nconstwlpolem  17115