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  831  rbaibd  832  syl3an9b  1204  sbcomxyyz  1843  eqeq12  2049  eleq12  2099  sbhypf  2597  ceqsrex2v  2670  sseq12  2962  rexprg  3413  rextpg  3415  breq12  3760  opelopabg  3996  brabg  3997  opelopab2  3998  ralxpf  4425  rexxpf  4426  feq23  4976  f00  5024  fconstg  5026  f1oeq23  5063  f1o00  5104  f1oiso  5408  riota1a  5430  cbvmpt2x  5524  caovord  5614  caovord3  5616  genpelvl  6495  genpelvu  6496  nn0ind-raph  8131  elfz  8650  elfzp12  8731