Theorem sylan9bb 451

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

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

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

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  sylan9bbr  452  bi2anan9  574  baibd  873  rbaibd  874  syl3an9b  1253  sbcomxyyz  1901  eqeq12  2107  eleq12  2159  sbhypf  2682  ceqsrex2v  2763  sseq12  3064  rexprg  3514  rextpg  3516  breq12  3872  opelopabg  4119  brabg  4120  opelopab2  4121  ralxpf  4613  rexxpf  4614  feq23  5182  f00  5237  fconstg  5242  f1oeq23  5282  f1o00  5323  f1oiso  5643  riota1a  5665  cbvmpt2x  5764  caovord  5854  caovord3  5856  genpelvl  7168  genpelvu  7169  nn0ind-raph  8962  xnn0xadd0  9433  elfz  9579  elfzp12  9662  shftfibg  10385  shftfib  10388  absdvdsb  11257  dvdsabsb  11258  dvdsabseq  11291  tgss2  11947  lmbr  12080  xmetec  12239