Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > simprl3 | Structured version Visualization version Unicode version |
Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
Ref | Expression |
---|---|
simprl3 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simpl3 1066 | . 2 | |
2 | 1 | adantl 482 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wi 4 wa 384 w3a 1037 |
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 df-3an 1039 |
This theorem is referenced by: pwfseqlem5 9485 icodiamlt 14174 issubc3 16509 pgpfac1lem5 18478 clsconn 21233 txlly 21439 txnlly 21440 itg2add 23526 ftc1a 23800 f1otrg 25751 ax5seglem6 25814 axcontlem10 25853 numclwwlk5 27246 locfinref 29908 noprefixmo 31848 nosupbnd2 31862 btwnouttr2 32129 btwnconn1lem13 32206 midofsegid 32211 outsideofeq 32237 ivthALT 32330 mpaaeu 37720 dfsalgen2 40559 |
Copyright terms: Public domain | W3C validator |