Theorem sylan9bb 438

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  439  bi2anan9  526  syl3an9b  1188  sbcomxyyz  1824  eqeq12  2030  eleq12  2080  sbhypf  2576  ceqsrex2v  2649  sseq12  2941  rexprg  3392  rextpg  3394  breq12  3739  opelopabg  3975  brabg  3976  opelopab2  3977  ralxpf  4405  rexxpf  4406  feq23  4955  f00  5002  fconstg  5004  f1oeq23  5041  f1o00  5082  f1oiso  5386  riota1a  5407  cbvmpt2x  5501  caovord  5591  caovord3  5593  genpelvl  6360  genpelvu  6361