Theorem sylan9r 360

Description: Nested syllogism inference conjoining dissimilar antecedents.

Hypotheses

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

Assertion

Ref	Expression
sylan9r	⊢ ((θ ∧ φ) → (ψ → τ))

Proof of Theorem sylan9r

Step	Hyp	Ref	Expression
1		sylan9r.1	. . 3 ⊢ (φ → (ψ → χ))
2		sylan9r.2	. . 3 ⊢ (θ → (χ → τ))
3	1, 2	syl9r 56	. 2 ⊢ (θ → (φ → (ψ → τ)))
4	3	imp 277	1 ⊢ ((θ ∧ φ) → (ψ → τ))

Syntax hints:   → wi 2   ∧ wa 196

This theorem is referenced by:  sbequi 876  limsssuc 2362  findsg 2398  tfinds 2401  tfindsg 2402  isofrlem 2939  f1oweOLD 2944  tfrlem8 2956  oaordi 3148  sdomdomtr 3370  pssnn 3428  inf3lem2 3465  r1tr 3498  rankr1 3518  zornlem7 3609  cardlim 3657  cardaleph 3690  cfub 3703  genpcd 3903  prlem934a 3931  uzwo 4605  nnwoOLD 4608  ocin 5177  spanun 5450

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