Theorem sylan9bb 462

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

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

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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  sylan9bbr  463  bi2anan9  606  baibd  924  rbaibd  925  syl3an9b  1321  sbcomxyyz  1988  eqeq12  2206  eleq12  2258  sbhypf  2809  ceqsrex2v  2892  sseq12  3204  rexprg  3670  rextpg  3672  breq12  4034  opelopabg  4298  brabg  4299  opelopabgf  4300  opelopab2  4301  ralxpf  4808  rexxpf  4809  feq23  5389  f00  5445  fconstg  5450  f1oeq23  5491  f1o00  5535  f1oiso  5869  riota1a  5893  cbvmpox  5996  caovord  6090  caovord3  6092  rbropapd  6295  genpelvl  7572  genpelvu  7573  nn0ind-raph  9434  elpq  9714  xnn0xadd0  9933  elfz  10080  elfzp12  10165  shftfibg  10964  shftfib  10967  absdvdsb  11952  dvdsabsb  11953  dvdsabseq  11989  islmod  13787  znidom  14145  tgss2  14247  lmbr  14381  xmetec  14605