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  3209  rexprg  3675  rextpg  3677  breq12  4039  opelopabg  4303  brabg  4304  opelopabgf  4305  opelopab2  4306  ralxpf  4813  rexxpf  4814  feq23  5396  f00  5452  fconstg  5457  f1oeq23  5498  f1o00  5542  f1oiso  5876  riota1a  5900  cbvmpox  6004  caovord  6099  caovord3  6101  rbropapd  6309  isacnm  7288  genpelvl  7598  genpelvu  7599  nn0ind-raph  9462  elpq  9742  xnn0xadd0  9961  elfz  10108  elfzp12  10193  shftfibg  11004  shftfib  11007  absdvdsb  11993  dvdsabsb  11994  dvdsabseq  12031  islmod  13925  znidom  14291  tgss2  14423  lmbr  14557  xmetec  14781  2lgslem1a  15437