Theorem sylan9bbr 419

Description: Nested syllogism inference conjoining dissimilar antecedents.

Hypotheses

Ref	Expression
sylan9bbr.1	⊢ (φ → (ψ ↔ χ))
sylan9bbr.2	⊢ (θ → (χ ↔ τ))

Assertion

Ref	Expression
sylan9bbr	⊢ ((θ ∧ φ) → (ψ ↔ τ))

Proof of Theorem sylan9bbr

Step	Hyp	Ref	Expression
1		sylan9bbr.1	. . 3 ⊢ (φ → (ψ ↔ χ))
2		sylan9bbr.2	. . 3 ⊢ (θ → (χ ↔ τ))
3	1, 2	sylan9bb 418	. 2 ⊢ ((φ ∧ θ) → (ψ ↔ τ))
4	3	ancoms 334	1 ⊢ ((θ ∧ φ) → (ψ ↔ τ))

Syntax hints:   → wi 2   ↔ wb 127   ∧ wa 196

This theorem is referenced by:  bimsc1 557  sbcom 916  sbcom2 992  otthg 1900  copsexg 1902  findsg 2398  tfindsg 2402  fconstfv 2903  f1oiso 2942  eloprabg 3035  oalimcl 3162  nnaordex 3191  nnawordex 3192  aceq6b 3565  ltmpi 3825  addclprlem1 3912  distrlem4pr 3924  1idpr 3927  prlem936a 3947  lt2sq 4414  nn1suc 4435  nn0ltp1let 4556  zaddclt 4590  qrecclt 4646  xpnnen 4927  znnen 4930  atcv1 5768

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6

This theorem depends on definitions:  df-bi 128  df-an 198

metamath.org