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  924  rbaibd  925  syl3an9b  1322  sbcomxyyz  1999  eqeq12  2217  eleq12  2269  sbhypf  2821  ceqsrex2v  2904  sseq12  3217  rexprg  3684  rextpg  3686  breq12  4048  opelopabg  4312  brabg  4313  opelopabgf  4314  opelopab2  4315  ralxpf  4822  rexxpf  4823  feq23  5405  f00  5461  fconstg  5466  f1oeq23  5507  f1o00  5551  f1oiso  5885  riota1a  5909  cbvmpox  6013  caovord  6108  caovord3  6110  rbropapd  6318  isacnm  7297  genpelvl  7607  genpelvu  7608  nn0ind-raph  9472  elpq  9752  xnn0xadd0  9971  elfz  10118  elfzp12  10203  shftfibg  11050  shftfib  11053  absdvdsb  12039  dvdsabsb  12040  dvdsabseq  12077  islmod  13971  znidom  14337  tgss2  14469  lmbr  14603  xmetec  14827  2lgslem1a  15483