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  610  baibd  931  rbaibd  932  syl3an9b  1347  sbcomxyyz  2028  eqeq12  2247  eleq12  2299  sbhypf  2866  ceqsrex2v  2952  sseq12  3267  rexprg  3746  rextpg  3748  breq12  4119  opelopabg  4391  brabg  4392  opelopabgf  4393  opelopab2  4394  ralxpf  4906  rexxpf  4907  feq23  5499  f00  5564  fconstg  5569  f1oeq23  5610  f1o00  5656  f1oiso  6005  riota1a  6032  cbvmpox  6139  caovord  6234  caovord3  6236  rbropapd  6486  suppeqfsuppbi  7261  isacnm  7523  genpelvl  7843  genpelvu  7844  nn0ind-raph  9713  elpq  9999  xnn0xadd0  10219  elfz  10367  elfzp12  10455  wrd2ind  11440  shftfibg  11530  shftfib  11533  absdvdsb  12520  dvdsabsb  12521  dvdsabseq  12558  islmod  14565  znidom  14931  tgss2  15070  lmbr  15204  xmetec  15428  2lgslem1a  16087  edgiedgbg  16186