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 987 | . 2 | |
2 | 1 | adantr 274 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wa 103 w3a 963 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 |
This theorem depends on definitions: df-bi 116 df-3an 965 |
This theorem is referenced by: frirrg 4310 fidceq 6814 fidifsnen 6815 en2eqpr 6852 iunfidisj 6890 ordiso2 6979 addlocpr 7456 aptiprlemu 7560 xltadd1 9780 xlesubadd 9787 icoshftf1o 9895 fztri3or 9941 elfzonelfzo 10129 exp3val 10421 hashun 10679 subcn2 11208 divalglemeuneg 11814 dvdslegcd 11848 lcmledvds 11947 rpdvds 11976 cncongr2 11981 iuncld 12526 iscnp4 12629 cnpnei 12630 cnconst2 12644 cnpdis 12653 txcn 12686 blssps 12838 blss 12839 metcnp3 12922 metcnp 12923 |
Copyright terms: Public domain | W3C validator |