![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > impel | Structured version Visualization version GIF version |
Description: An inference for implication elimination. (Contributed by Giovanni Mascellani, 23-May-2019.) (Proof shortened by Wolf Lammen, 2-Sep-2020.) |
Ref | Expression |
---|---|
impel.1 | ⊢ (𝜑 → (𝜓 → 𝜒)) |
impel.2 | ⊢ (𝜃 → 𝜓) |
Ref | Expression |
---|---|
impel | ⊢ ((𝜑 ∧ 𝜃) → 𝜒) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | impel.2 | . . 3 ⊢ (𝜃 → 𝜓) | |
2 | impel.1 | . . 3 ⊢ (𝜑 → (𝜓 → 𝜒)) | |
3 | 1, 2 | syl5 34 | . 2 ⊢ (𝜑 → (𝜃 → 𝜒)) |
4 | 3 | imp 396 | 1 ⊢ ((𝜑 ∧ 𝜃) → 𝜒) |
Colors of variables: wff setvar class |
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 |
Copyright terms: Public domain | W3C validator |