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  2026  eqeq12  2245  eleq12  2297  sbhypf  2864  ceqsrex2v  2949  sseq12  3263  rexprg  3741  rextpg  3743  breq12  4114  opelopabg  4386  brabg  4387  opelopabgf  4388  opelopab2  4389  ralxpf  4901  rexxpf  4902  feq23  5494  f00  5559  fconstg  5564  f1oeq23  5605  f1o00  5651  f1oiso  5999  riota1a  6024  cbvmpox  6131  caovord  6226  caovord3  6228  rbropapd  6473  suppeqfsuppbi  7248  isacnm  7510  genpelvl  7827  genpelvu  7828  nn0ind-raph  9695  elpq  9981  xnn0xadd0  10200  elfz  10348  elfzp12  10433  wrd2ind  11415  shftfibg  11505  shftfib  11508  absdvdsb  12495  dvdsabsb  12496  dvdsabseq  12533  islmod  14439  znidom  14805  tgss2  14944  lmbr  15078  xmetec  15302  2lgslem1a  15961  edgiedgbg  16060