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  2810  ceqsrex2v  2893  sseq12  3205  rexprg  3671  rextpg  3673  breq12  4035  opelopabg  4299  brabg  4300  opelopabgf  4301  opelopab2  4302  ralxpf  4809  rexxpf  4810  feq23  5390  f00  5446  fconstg  5451  f1oeq23  5492  f1o00  5536  f1oiso  5870  riota1a  5894  cbvmpox  5997  caovord  6092  caovord3  6094  rbropapd  6297  genpelvl  7574  genpelvu  7575  nn0ind-raph  9437  elpq  9717  xnn0xadd0  9936  elfz  10083  elfzp12  10168  shftfibg  10967  shftfib  10970  absdvdsb  11955  dvdsabsb  11956  dvdsabseq  11992  islmod  13790  znidom  14156  tgss2  14258  lmbr  14392  xmetec  14616  2lgslem1a  15245