![]() |
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 1002 |
. 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 980 |
This theorem is referenced by: frirrg 4350 fidceq 6868 fidifsnen 6869 en2eqpr 6906 iunfidisj 6944 ordiso2 7033 addlocpr 7534 aptiprlemu 7638 xltadd1 9874 xlesubadd 9881 icoshftf1o 9989 fztri3or 10036 elfzonelfzo 10227 exp3val 10519 nn0ltexp2 10685 hashun 10780 subcn2 11314 divalglemeuneg 11922 dvdslegcd 11959 lcmledvds 12064 rpdvds 12093 cncongr2 12098 qexpz 12344 iuncld 13508 iscnp4 13611 cnpnei 13612 cnconst2 13626 cnpdis 13635 txcn 13668 blssps 13820 blss 13821 metcnp3 13904 metcnp 13905 lgsfcl2 14300 lgsdir 14329 lgsne0 14332 |
Copyright terms: Public domain | W3C validator |