![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > pm2.43d | Structured version Visualization version GIF version |
Description: Deduction absorbing redundant antecedent. Deduction associated with pm2.43 56 and pm2.43i 52. (Contributed by NM, 18-Aug-1993.) (Proof shortened by Mel L. O'Cat, 28-Nov-2008.) |
Ref | Expression |
---|---|
pm2.43d.1 | ⊢ (𝜑 → (𝜓 → (𝜓 → 𝜒))) |
Ref | Expression |
---|---|
pm2.43d | ⊢ (𝜑 → (𝜓 → 𝜒)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | id 22 | . 2 ⊢ (𝜓 → 𝜓) | |
2 | pm2.43d.1 | . 2 ⊢ (𝜑 → (𝜓 → (𝜓 → 𝜒))) | |
3 | 1, 2 | mpdi 45 | 1 ⊢ (𝜑 → (𝜓 → 𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 |
This theorem is referenced by: loolin 111 rspct 3567 po2nr 5559 somo 5582 ordelord 6339 tz7.7 6343 funssres 6545 2elresin 6622 dffv2 6936 f1imass 7210 onint 7724 wfrlem12OLD 8265 wfrlem14OLD 8267 onfununi 8286 smoel 8305 tfrlem11 8333 tfr3 8344 omass 8526 nnmass 8570 sbthlem1 9026 pssnn 9111 php 9153 phpOLD 9165 inf3lem2 9564 cardne 9900 dfac2b 10065 indpi 10842 genpcd 10941 ltexprlem7 10977 addcanpr 10981 reclem4pr 10985 suplem2pr 10988 sup2 12110 nnunb 12408 uzwo 12835 xrub 13230 grpid 18785 lsmcss 21094 uniopn 22244 fclsss1 23371 fclsss2 23372 sltval2 27002 grpoid 29409 spansncvi 30541 pjnormssi 31057 sumdmdlem2 31308 acycgrcycl 33681 meran1 34873 bj-animbi 35012 currysetlem2 35409 bj-elsn0 35616 poimirlem31 36099 heicant 36103 hlhilhillem 40417 sn-sup2 40915 ee223 42897 eel2122old 42981 afv0nbfvbi 45354 fmtnoprmfac1lem 45727 |
Copyright terms: Public domain | W3C validator |