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  6795  elfi  7310  ltmpig  7712  mul0eqap  9008  qreccl  10058  0fz1  10466  zmodid2  10810  ccatrcl1  11404  divgcdcoprm0  12904  sscntz  14158  cnptoprest  15465  txrest  15502  uhgreq12g  16522  cbvrald  17021