Theorem impel 502

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 34	. 2 ⊢ (𝜑 → (𝜃 → 𝜒))
4	3	imp 396	1 ⊢ ((𝜑 ∧ 𝜃) → 𝜒)

Syntax hints:   → wi 4   ∧ wa 385

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

This theorem depends on definitions:  df-bi 199  df-an 386

This theorem is referenced by:  equs5e  2465  elabgt  3536  mob2  3581  ssn0rex  4135  reusv2lem2  5068  copsex2t  5146  trssord  5957  trsuc  6024  wfrlem4  7655  ectocld  8051  fiint  8478  eqinf  8631  lcmfunsnlem2lem2  15684  gsummoncoe1  19993  tnggrpr  22784  wlkv0  26893  wlkp1lem1  26919  wlkswwlksf1o  27129  wspniunwspnon  27205  wwlksext2clwwlkOLD  27367  trlsegvdeglem1  27558  frcond4  27612  2clwwlk2clwwlk  27697  2clwwlk2clwwlkOLD  27698  opabssi  29935  frrlem4  32289  noresle  32352  bj-restpw  33531  cnfinltrel  33732  cover2  33989  setindtr  38365  climxlim2lem  40804  lighneallem4  42298  proththd  42302