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  968  mpteq12f  4167  opelopabsb  4352  elrelimasn  5100  fvelrnb  5689  fmptco  5809  fconstfvm  5867  f1oiso  5962  canth  5964  mpoeq123  6075  elovmporab  6217  elovmporab1w  6218  dfoprab4f  6351  fmpox  6360  nnmword  6681  elfi  7161  ltmpig  7549  mul0eqap  8840  qreccl  9866  0fz1  10270  zmodid2  10604  ccatrcl1  11181  divgcdcoprm0  12663  cnptoprest  14953  txrest  14990  uhgreq12g  15917  cbvrald  16320