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  610  baibd  931  rbaibd  932  syl3an9b  1347  sbcomxyyz  2025  eqeq12  2244  eleq12  2296  sbhypf  2854  ceqsrex2v  2939  sseq12  3253  rexprg  3725  rextpg  3727  breq12  4098  opelopabg  4368  brabg  4369  opelopabgf  4370  opelopab2  4371  ralxpf  4882  rexxpf  4883  feq23  5475  f00  5537  fconstg  5542  f1oeq23  5583  f1o00  5629  f1oiso  5977  riota1a  6002  cbvmpox  6109  caovord  6204  caovord3  6206  rbropapd  6451  isacnm  7461  genpelvl  7775  genpelvu  7776  nn0ind-raph  9641  elpq  9927  xnn0xadd0  10146  elfz  10294  elfzp12  10379  wrd2ind  11353  shftfibg  11443  shftfib  11446  absdvdsb  12433  dvdsabsb  12434  dvdsabseq  12471  islmod  14370  znidom  14736  tgss2  14873  lmbr  15007  xmetec  15231  2lgslem1a  15890  edgiedgbg  15989