Theorem sylan9bb 459

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 274	. 2 ⊢ ((𝜑 ∧ 𝜃) → (𝜓 ↔ 𝜒))
3		sylan9bb.2	. . 3 ⊢ (𝜃 → (𝜒 ↔ 𝜏))
4	3	adantl 275	. 2 ⊢ ((𝜑 ∧ 𝜃) → (𝜒 ↔ 𝜏))
5	2, 4	bitrd 187	1 ⊢ ((𝜑 ∧ 𝜃) → (𝜓 ↔ 𝜏))

Syntax hints:   → wi 4   ∧ wa 103   ↔ wb 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  sylan9bbr  460  bi2anan9  601  baibd  918  rbaibd  919  syl3an9b  1305  sbcomxyyz  1965  eqeq12  2183  eleq12  2235  sbhypf  2779  ceqsrex2v  2862  sseq12  3172  rexprg  3633  rextpg  3635  breq12  3992  opelopabg  4251  brabg  4252  opelopab2  4253  ralxpf  4755  rexxpf  4756  feq23  5331  f00  5387  fconstg  5392  f1oeq23  5432  f1o00  5475  f1oiso  5802  riota1a  5825  cbvmpox  5928  caovord  6021  caovord3  6023  rbropapd  6218  genpelvl  7461  genpelvu  7462  nn0ind-raph  9316  elpq  9594  xnn0xadd0  9811  elfz  9958  elfzp12  10042  shftfibg  10771  shftfib  10774  absdvdsb  11758  dvdsabsb  11759  dvdsabseq  11794  tgss2  12832  lmbr  12966  xmetec  13190