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  930  rbaibd  931  syl3an9b  1346  sbcomxyyz  2025  eqeq12  2244  eleq12  2296  sbhypf  2853  ceqsrex2v  2938  sseq12  3252  rexprg  3721  rextpg  3723  breq12  4093  opelopabg  4362  brabg  4363  opelopabgf  4364  opelopab2  4365  ralxpf  4876  rexxpf  4877  feq23  5468  f00  5528  fconstg  5533  f1oeq23  5574  f1o00  5620  f1oiso  5966  riota1a  5991  cbvmpox  6098  caovord  6193  caovord3  6195  rbropapd  6407  isacnm  7417  genpelvl  7731  genpelvu  7732  nn0ind-raph  9596  elpq  9882  xnn0xadd0  10101  elfz  10248  elfzp12  10333  wrd2ind  11303  shftfibg  11380  shftfib  11383  absdvdsb  12369  dvdsabsb  12370  dvdsabseq  12407  islmod  14304  znidom  14670  tgss2  14802  lmbr  14936  xmetec  15160  2lgslem1a  15816  edgiedgbg  15915