| Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > ILE Home > Th. List > simpll3 | Unicode version | ||
| Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| Ref | Expression |
|---|---|
| simpll3 |
|
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | simpl3 1005 |
. 2
| |
| 2 | 1 | adantr 276 |
1
|
| Colors of variables: wff set class |
| Syntax hints: |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 |
| This theorem depends on definitions: df-bi 117 df-3an 983 |
| This theorem is referenced by: frirrg 4397 fidceq 6966 fidifsnen 6967 en2eqpr 7004 iunfidisj 7048 ordiso2 7137 addlocpr 7649 aptiprlemu 7753 xltadd1 9998 xlesubadd 10005 icoshftf1o 10113 fztri3or 10161 elfzonelfzo 10359 exp3val 10686 nn0ltexp2 10854 hashun 10950 swrdclg 11103 subcn2 11622 divalglemeuneg 12234 dvdslegcd 12285 lcmledvds 12392 rpdvds 12421 cncongr2 12426 qexpz 12675 iuncld 14587 iscnp4 14690 cnpnei 14691 cnconst2 14705 cnpdis 14714 txcn 14747 blssps 14899 blss 14900 metcnp3 14983 metcnp 14984 lgsfcl2 15483 lgsdir 15512 lgsne0 15515 |
| Copyright terms: Public domain | W3C validator |