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  1991  eqeq12  2209  eleq12  2261  sbhypf  2813  ceqsrex2v  2896  sseq12  3208  rexprg  3674  rextpg  3676  breq12  4038  opelopabg  4302  brabg  4303  opelopabgf  4304  opelopab2  4305  ralxpf  4812  rexxpf  4813  feq23  5393  f00  5449  fconstg  5454  f1oeq23  5495  f1o00  5539  f1oiso  5873  riota1a  5897  cbvmpox  6000  caovord  6095  caovord3  6097  rbropapd  6300  genpelvl  7579  genpelvu  7580  nn0ind-raph  9443  elpq  9723  xnn0xadd0  9942  elfz  10089  elfzp12  10174  shftfibg  10985  shftfib  10988  absdvdsb  11974  dvdsabsb  11975  dvdsabseq  12012  islmod  13847  znidom  14213  tgss2  14315  lmbr  14449  xmetec  14673  2lgslem1a  15329