Theorem sylan9bb 466

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 ⊢ ((𝜑 ∧ 𝜃) → (𝜓 ↔ 𝜏))

This proof depends on syntax axioms:   → wi 4   ∧ wa 104   ↔ wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  sylan9bbr  467  bi2anan9  614  baibd  935  rbaibd  936  syl3an9b  1351  sbcomxyyz  2032  eqeq12  2251  eleq12  2303  sbhypf  2872  ceqsrex2v  2958  sseq12  3273  rexprg  3761  rextpg  3763  breq12  4135  opelopabg  4410  brabg  4411  opelopabgf  4412  opelopab2  4413  ralxpf  4926  rexxpf  4927  feq23  5519  f00  5584  fconstg  5589  f1oeq23  5630  f1o00  5676  f1oiso  6032  riota1a  6059  cbvmpox  6166  caovord  6261  caovord3  6263  rbropapd  6513  suppeqfsuppbi  7295  isacnm  7560  genpelvl  7880  genpelvu  7881  nn0ind-raph  9768  elpq  10060  xnn0xadd0  10280  elfz  10428  elfzp12  10517  wrd2ind  11511  shftfibg  11601  shftfib  11604  absdvdsb  12595  dvdsabsb  12596  dvdsabseq  12633  islmod  14711  znidom  15076  tgss2  15271  lmbr  15405  xmetec  15629  2lgslem1a  16373  edgiedgbg  16472