Theorem sylan9bb 435

Description: Nested syllogism inference conjoining dissimilar antecedents. (Contributed by NM, 4-Mar-1995.)

Hypotheses

Ref	Expression
sylan9bb.1	⊢ (𝜑 → (𝜓 ↔ 𝜒))
sylan9bb.2	⊢ (𝜃 → (𝜒 ↔ 𝜏))

Assertion

Ref	Expression
sylan9bb	⊢ ((𝜑 ∧ 𝜃) → (𝜓 ↔ 𝜏))

Proof of Theorem sylan9bb

Step	Hyp	Ref	Expression
1		sylan9bb.1	. . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
2	1	adantr 261	. 2 ⊢ ((𝜑 ∧ 𝜃) → (𝜓 ↔ 𝜒))
3		sylan9bb.2	. . 3 ⊢ (𝜃 → (𝜒 ↔ 𝜏))
4	3	adantl 262	. 2 ⊢ ((𝜑 ∧ 𝜃) → (𝜒 ↔ 𝜏))
5	2, 4	bitrd 177	1 ⊢ ((𝜑 ∧ 𝜃) → (𝜓 ↔ 𝜏))

Syntax hints:   → wi 4   ∧ wa 97   ↔ wb 98

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101

This theorem depends on definitions:  df-bi 110

This theorem is referenced by:  sylan9bbr  436  bi2anan9  538  baibd  832  rbaibd  833  syl3an9b  1205  sbcomxyyz  1846  eqeq12  2052  eleq12  2102  sbhypf  2603  ceqsrex2v  2676  sseq12  2968  rexprg  3422  rextpg  3424  breq12  3769  opelopabg  4005  brabg  4006  opelopab2  4007  ralxpf  4482  rexxpf  4483  feq23  5033  f00  5081  fconstg  5083  f1oeq23  5120  f1o00  5161  f1oiso  5465  riota1a  5487  cbvmpt2x  5582  caovord  5672  caovord3  5674  genpelvl  6610  genpelvu  6611  nn0ind-raph  8355  elfz  8880  elfzp12  8961  shftfibg  9421  shftfib  9424