Theorem sylan9bb 457

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  458  bi2anan9  595  baibd  908  rbaibd  909  syl3an9b  1288  sbcomxyyz  1943  eqeq12  2150  eleq12  2202  sbhypf  2730  ceqsrex2v  2812  sseq12  3117  rexprg  3570  rextpg  3572  breq12  3929  opelopabg  4185  brabg  4186  opelopab2  4187  ralxpf  4680  rexxpf  4681  feq23  5253  f00  5309  fconstg  5314  f1oeq23  5354  f1o00  5395  f1oiso  5720  riota1a  5742  cbvmpox  5842  caovord  5935  caovord3  5937  rbropapd  6132  genpelvl  7313  genpelvu  7314  nn0ind-raph  9161  xnn0xadd0  9643  elfz  9789  elfzp12  9872  shftfibg  10585  shftfib  10588  absdvdsb  11500  dvdsabsb  11501  dvdsabseq  11534  tgss2  12237  lmbr  12371  xmetec  12595