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  608  baibd  928  rbaibd  929  syl3an9b  1344  sbcomxyyz  2023  eqeq12  2242  eleq12  2294  sbhypf  2850  ceqsrex2v  2935  sseq12  3249  rexprg  3718  rextpg  3720  breq12  4087  opelopabg  4355  brabg  4356  opelopabgf  4357  opelopab2  4358  ralxpf  4867  rexxpf  4868  feq23  5458  f00  5516  fconstg  5521  f1oeq23  5562  f1o00  5607  f1oiso  5949  riota1a  5974  cbvmpox  6081  caovord  6176  caovord3  6178  rbropapd  6386  isacnm  7381  genpelvl  7695  genpelvu  7696  nn0ind-raph  9560  elpq  9840  xnn0xadd0  10059  elfz  10206  elfzp12  10291  wrd2ind  11250  shftfibg  11326  shftfib  11329  absdvdsb  12315  dvdsabsb  12316  dvdsabseq  12353  islmod  14249  znidom  14615  tgss2  14747  lmbr  14881  xmetec  15105  2lgslem1a  15761  edgiedgbg  15859