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

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  975  mpteq12f  4206  opelopabsb  4397  elrelimasn  5148  fvelrnb  5744  fmptco  5865  fconstfvm  5924  f1oiso  6022  canth  6026  mpoeq123  6137  elovmporab  6279  elovmporab1w  6280  dfoprab4f  6417  fmpox  6426  nnmword  6781  elfi  7295  ltmpig  7696  mul0eqap  8990  qreccl  10021  0fz1  10428  zmodid2  10767  ccatrcl1  11360  divgcdcoprm0  12857  cnptoprest  15263  txrest  15300  uhgreq12g  16231  cbvrald  16730