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  923  rbaibd  924  syl3an9b  1310  sbcomxyyz  1972  eqeq12  2190  eleq12  2242  sbhypf  2786  ceqsrex2v  2869  sseq12  3180  rexprg  3644  rextpg  3646  breq12  4008  opelopabg  4268  brabg  4269  opelopab2  4270  ralxpf  4773  rexxpf  4774  feq23  5351  f00  5407  fconstg  5412  f1oeq23  5452  f1o00  5496  f1oiso  5826  riota1a  5849  cbvmpox  5952  caovord  6045  caovord3  6047  rbropapd  6242  genpelvl  7510  genpelvu  7511  nn0ind-raph  9369  elpq  9647  xnn0xadd0  9866  elfz  10013  elfzp12  10098  shftfibg  10828  shftfib  10831  absdvdsb  11815  dvdsabsb  11816  dvdsabseq  11852  islmod  13379  tgss2  13549  lmbr  13683  xmetec  13907