Theorem syl3anbrc 1088

Description: Syllogism inference. (Contributed by Mario Carneiro, 11-May-2014.)

Hypotheses

Ref	Expression
syl3anbrc.1	⊢ (𝜑 → 𝜓)
syl3anbrc.2	⊢ (𝜑 → 𝜒)
syl3anbrc.3	⊢ (𝜑 → 𝜃)
syl3anbrc.4	⊢ (𝜏 ↔ (𝜓 ∧ 𝜒 ∧ 𝜃))

Assertion

Ref	Expression
syl3anbrc	⊢ (𝜑 → 𝜏)

Proof of Theorem syl3anbrc

Step	Hyp	Ref	Expression
1		syl3anbrc.1	. . 3 ⊢ (𝜑 → 𝜓)
2		syl3anbrc.2	. . 3 ⊢ (𝜑 → 𝜒)
3		syl3anbrc.3	. . 3 ⊢ (𝜑 → 𝜃)
4	1, 2, 3	3jca 1084	. 2 ⊢ (𝜑 → (𝜓 ∧ 𝜒 ∧ 𝜃))
5		syl3anbrc.4	. 2 ⊢ (𝜏 ↔ (𝜓 ∧ 𝜒 ∧ 𝜃))
6	4, 5	sylibr 137	1 ⊢ (𝜑 → 𝜏)

Syntax hints:   → wi 4   ↔ wb 98   ∧ w3a 885

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101

This theorem depends on definitions:  df-bi 110  df-3an 887

This theorem is referenced by:  smores2  5909  smoiso  5917  iserd  6132  xpiderm  6177  erinxp  6180  prarloc  6601  eluzuzle  8481  uztrn  8489  nn0pzuz  8530  nn0ge2m1nnALT  8553  ige2m1fz  8972  0elfz  8977  elfz0addOLD  8980  uzsubfz0  8986  elfzmlbm  8988  difelfzle  8992  difelfznle  8993  elfzolt2b  9014  elfzolt3b  9015  elfzouz2  9017  fzossrbm1  9029  elfzo0  9038  eluzgtdifelfzo  9053  elfzodifsumelfzo  9057  fzonn0p1  9067  fzonn0p1p1  9069  elfzom1p1elfzo  9070  fzo0sn0fzo1  9077  ssfzo12bi  9081  ubmelm1fzo  9082  elfzonelfzo  9086  fzosplitprm1  9090  fzostep1  9093  fvinim0ffz  9096  flqword2  9131  resqrexlemoverl  9619