Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > anabsi5 | Structured version Visualization version Unicode version |
Description: Absorption of antecedent into conjunction. (Contributed by NM, 11-Jun-1995.) (Proof shortened by Wolf Lammen, 18-Nov-2013.) |
Ref | Expression |
---|---|
anabsi5.1 |
Ref | Expression |
---|---|
anabsi5 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | anabsi5.1 | . . 3 | |
2 | 1 | imp 445 | . 2 |
3 | 2 | anabss5 857 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wi 4 wa 384 |
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 197 df-an 386 |
This theorem is referenced by: anabsi6 859 anabsi8 861 3anidm12 1383 rspce 3304 onint 6995 f1oweALT 7152 php2 8145 hasheqf1oi 13140 hasheqf1oiOLD 13141 rtrclreclem3 13800 rtrclreclem4 13801 ptcmpfi 21616 redwlk 26569 frgruhgr0v 27127 finxpreclem2 33227 finxpreclem6 33233 diophin 37336 diophun 37337 rspcegf 39182 stoweidlem36 40253 |
Copyright terms: Public domain | W3C validator |