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  608  baibd  928  rbaibd  929  syl3an9b  1344  sbcomxyyz  2023  eqeq12  2242  eleq12  2294  sbhypf  2851  ceqsrex2v  2936  sseq12  3250  rexprg  3719  rextpg  3721  breq12  4091  opelopabg  4360  brabg  4361  opelopabgf  4362  opelopab2  4363  ralxpf  4874  rexxpf  4875  feq23  5465  f00  5525  fconstg  5530  f1oeq23  5571  f1o00  5616  f1oiso  5962  riota1a  5987  cbvmpox  6094  caovord  6189  caovord3  6191  rbropapd  6403  isacnm  7408  genpelvl  7722  genpelvu  7723  nn0ind-raph  9587  elpq  9873  xnn0xadd0  10092  elfz  10239  elfzp12  10324  wrd2ind  11294  shftfibg  11371  shftfib  11374  absdvdsb  12360  dvdsabsb  12361  dvdsabseq  12398  islmod  14295  znidom  14661  tgss2  14793  lmbr  14927  xmetec  15151  2lgslem1a  15807  edgiedgbg  15906