![]() |
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 397 | 1 ⊢ ((𝜑 ∧ 𝜃) → 𝜒) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 386 |
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 387 |
This theorem is referenced by: equs5e 2424 elabgt 3553 mob2 3598 ssn0rex 4164 reusv2lem2 5113 copsex2t 5190 trssord 5995 trsuc 6062 funimass2 6219 fvelima 6510 fvmptf 6564 funfvima2 6767 funfvima3 6770 tfi 7333 suppssov1 7611 tposf2 7660 wfrlem4 7702 wfrlem10 7709 ectocld 8099 mapsnd 8185 resixpfo 8234 f1oeng 8262 nneneq 8433 nnsdomg 8509 fiint 8527 fodomfi 8529 eqinf 8680 hartogslem1 8738 cantnf 8889 rankwflemb 8955 carden2a 9127 carduni 9142 harval2 9158 cardaleph 9247 alephval3 9268 dfac5 9286 cfcof 9433 axdc4lem 9614 nqereu 10088 recexsr 10266 seqcoll 13568 swrdswrd 13820 swrdccatin2 13862 repswswrd 13936 climcau 14818 odd2np1 15479 lcmfunsnlem2lem2 15768 coprmproddvdslem 15791 dvdsprm 15830 vdwlem6 16105 imasvscafn 16594 dirref 17632 irredn1 19104 isdrngd 19175 gsummoncoe1 20081 psgnghm 20332 prdstopn 21851 cnextcn 22290 tnggrpr 22878 ovolctb 23705 dyadmbl 23815 itg1addlem4 23914 itg1le 23928 wlkv0 27015 wlkp1lem1 27041 wlkswwlksf1o 27245 wspniunwspnon 27320 trlsegvdeglem1 27641 frcond4 27695 2clwwlk2clwwlk 27778 2clwwlk2clwwlkOLD 27779 opabssi 30005 frrlem4 32380 noresle 32443 bj-restpw 33626 cnfinltrel 33843 cover2 34142 setindtr 38564 climxlim2lem 40999 2reuimp 42170 lighneallem4 42562 proththd 42566 lincresunit3 43299 |
Copyright terms: Public domain | W3C validator |