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  4212  opelopabsb  4404  elrelimasn  5156  fvelrnb  5753  fmptco  5877  fconstfvm  5936  f1oiso  6035  canth  6039  mpoeq123  6150  elovmporab  6292  elovmporab1w  6293  dfoprab4f  6431  fmpox  6440  nnmword  6796  elfi  7310  ltmpig  7712  mul0eqap  9008  qreccl  10057  0fz1  10465  zmodid2  10809  ccatrcl1  11403  divgcdcoprm0  12903  sscntz  14157  cnptoprest  15482  txrest  15519  uhgreq12g  16539  cbvrald  17038