Theorem sylan9bbr 467

Description: Nested syllogism inference conjoining dissimilar antecedents. (Contributed by NM, 4-Mar-1995.)

Hypotheses

Ref	Expression
sylan9bbr.1	⊢ (𝜑 → (𝜓 ↔ 𝜒))
sylan9bbr.2	⊢ (𝜃 → (𝜒 ↔ 𝜏))

Assertion

Ref	Expression
sylan9bbr	⊢ ((𝜃 ∧ 𝜑) → (𝜓 ↔ 𝜏))

Proof of Theorem sylan9bbr

Step	Hyp	Ref	Expression
1		sylan9bbr.1	. . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
2		sylan9bbr.2	. . 3 ⊢ (𝜃 → (𝜒 ↔ 𝜏))
3	1, 2	sylan9bb 466	. 2 ⊢ ((𝜑 ∧ 𝜃) → (𝜓 ↔ 𝜏))
4	3	ancoms 268	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:  pm5.75  975  mpteq12f  4211  opelopabsb  4402  elrelimasn  5153  fvelrnb  5750  fmptco  5874  fconstfvm  5933  f1oiso  6032  canth  6036  mpoeq123  6147  elovmporab  6289  elovmporab1w  6290  dfoprab4f  6427  fmpox  6436  nnmword  6791  elfi  7305  ltmpig  7706  mul0eqap  9000  qreccl  10042  0fz1  10449  zmodid2  10789  ccatrcl1  11382  divgcdcoprm0  12879  cnptoprest  15340  txrest  15377  uhgreq12g  16317  cbvrald  16816