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  606  baibd  923  rbaibd  924  syl3an9b  1310  sbcomxyyz  1972  eqeq12  2190  eleq12  2242  sbhypf  2788  ceqsrex2v  2871  sseq12  3182  rexprg  3646  rextpg  3648  breq12  4010  opelopabg  4270  brabg  4271  opelopab2  4272  ralxpf  4775  rexxpf  4776  feq23  5353  f00  5409  fconstg  5414  f1oeq23  5454  f1o00  5498  f1oiso  5829  riota1a  5852  cbvmpox  5955  caovord  6048  caovord3  6050  rbropapd  6245  genpelvl  7513  genpelvu  7514  nn0ind-raph  9372  elpq  9650  xnn0xadd0  9869  elfz  10016  elfzp12  10101  shftfibg  10831  shftfib  10834  absdvdsb  11818  dvdsabsb  11819  dvdsabseq  11855  islmod  13386  tgss2  13618  lmbr  13752  xmetec  13976