Theorem sylan9bb 458

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 274	. 2 ⊢ ((𝜑 ∧ 𝜃) → (𝜓 ↔ 𝜒))
3		sylan9bb.2	. . 3 ⊢ (𝜃 → (𝜒 ↔ 𝜏))
4	3	adantl 275	. 2 ⊢ ((𝜑 ∧ 𝜃) → (𝜒 ↔ 𝜏))
5	2, 4	bitrd 187	1 ⊢ ((𝜑 ∧ 𝜃) → (𝜓 ↔ 𝜏))

Syntax hints:   → wi 4   ∧ wa 103   ↔ wb 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  sylan9bbr  459  bi2anan9  596  baibd  909  rbaibd  910  syl3an9b  1289  sbcomxyyz  1946  eqeq12  2153  eleq12  2205  sbhypf  2738  ceqsrex2v  2821  sseq12  3127  rexprg  3583  rextpg  3585  breq12  3942  opelopabg  4198  brabg  4199  opelopab2  4200  ralxpf  4693  rexxpf  4694  feq23  5266  f00  5322  fconstg  5327  f1oeq23  5367  f1o00  5410  f1oiso  5735  riota1a  5757  cbvmpox  5857  caovord  5950  caovord3  5952  rbropapd  6147  genpelvl  7344  genpelvu  7345  nn0ind-raph  9192  elpq  9467  xnn0xadd0  9680  elfz  9827  elfzp12  9910  shftfibg  10624  shftfib  10627  absdvdsb  11547  dvdsabsb  11548  dvdsabseq  11581  tgss2  12287  lmbr  12421  xmetec  12645