Theorem impel 280

Description: An inference for implication elimination. (Contributed by Giovanni Mascellani, 23-May-2019.) (Proof shortened by Wolf Lammen, 2-Sep-2020.)

Hypotheses

Ref	Expression
impel.1	⊢ (𝜑 → (𝜓 → 𝜒))
impel.2	⊢ (𝜃 → 𝜓)

Assertion

Ref	Expression
impel	⊢ ((𝜑 ∧ 𝜃) → 𝜒)

Proof of Theorem impel

Step	Hyp	Ref	Expression
1		impel.2	. . 3 ⊢ (𝜃 → 𝜓)
2		impel.1	. . 3 ⊢ (𝜑 → (𝜓 → 𝜒))
3	1, 2	syl5 32	. 2 ⊢ (𝜑 → (𝜃 → 𝜒))
4	3	imp 124	1 ⊢ ((𝜑 ∧ 𝜃) → 𝜒)

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

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

This theorem is used by:  pm4.55dc  951  mapsnd  6970  fiintim  7238  eqinfti  7360  finomni  7480  frecuzrdgrclt  10852  seq3coll  11294  swrdswrd  11477  swrdccatin1  11497  swrdccatin2  11501  fprodsplitsn  12400  nninfctlemfo  12817  unct  13333  isnzr2  14491  dvcnp2cntop  15800  fsumdvdsmul  16105  perfectlem2  16114  upgrwlkcompim  16603  wlkv0  16610  trlsegvdeglem1  16701