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  4088  opelopabg  4356  brabg  4357  opelopabgf  4358  opelopab2  4359  ralxpf  4868  rexxpf  4869  feq23  5459  f00  5519  fconstg  5524  f1oeq23  5565  f1o00  5610  f1oiso  5956  riota1a  5981  cbvmpox  6088  caovord  6183  caovord3  6185  rbropapd  6394  isacnm  7396  genpelvl  7710  genpelvu  7711  nn0ind-raph  9575  elpq  9856  xnn0xadd0  10075  elfz  10222  elfzp12  10307  wrd2ind  11270  shftfibg  11346  shftfib  11349  absdvdsb  12335  dvdsabsb  12336  dvdsabseq  12373  islmod  14270  znidom  14636  tgss2  14768  lmbr  14902  xmetec  15126  2lgslem1a  15782  edgiedgbg  15880