Theorem sylan9bbr 463

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 462	. 2 ⊢ ((𝜑 ∧ 𝜃) → (𝜓 ↔ 𝜏))
4	3	ancoms 268	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:  pm5.75  971  mpteq12f  4195  opelopabsb  4383  elrelimasn  5133  fvelrnb  5729  fmptco  5848  fconstfvm  5907  f1oiso  6005  canth  6009  mpoeq123  6120  elovmporab  6262  elovmporab1w  6263  dfoprab4f  6400  fmpox  6409  nnmword  6764  elfi  7271  ltmpig  7670  mul0eqap  8961  qreccl  9992  0fz1  10399  zmodid2  10738  ccatrcl1  11327  divgcdcoprm0  12823  cnptoprest  15230  txrest  15267  uhgreq12g  16197  cbvrald  16686