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  925  rbaibd  926  syl3an9b  1323  sbcomxyyz  2001  eqeq12  2219  eleq12  2271  sbhypf  2824  ceqsrex2v  2909  sseq12  3222  rexprg  3690  rextpg  3692  breq12  4056  opelopabg  4322  brabg  4323  opelopabgf  4324  opelopab2  4325  ralxpf  4832  rexxpf  4833  feq23  5421  f00  5479  fconstg  5484  f1oeq23  5525  f1o00  5570  f1oiso  5908  riota1a  5932  cbvmpox  6036  caovord  6131  caovord3  6133  rbropapd  6341  isacnm  7331  genpelvl  7645  genpelvu  7646  nn0ind-raph  9510  elpq  9790  xnn0xadd0  10009  elfz  10156  elfzp12  10241  wrd2ind  11199  shftfibg  11206  shftfib  11209  absdvdsb  12195  dvdsabsb  12196  dvdsabseq  12233  islmod  14128  znidom  14494  tgss2  14626  lmbr  14760  xmetec  14984  2lgslem1a  15640  edgiedgbg  15736