Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > 3simpa | Unicode version |
Description: Simplification of triple conjunction. (Contributed by NM, 21-Apr-1994.) |
Ref | Expression |
---|---|
3simpa |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-3an 949 | . 2 | |
2 | 1 | simplbi 272 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wa 103 w3a 947 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 |
This theorem depends on definitions: df-bi 116 df-3an 949 |
This theorem is referenced by: 3simpb 964 3simpc 965 simp1 966 simp2 967 3adant3 986 3adantl3 1124 3adantr3 1127 opprc 3696 oprcl 3699 opm 4126 funtpg 5144 ftpg 5572 ovig 5860 prltlu 7263 mullocpr 7347 lt2halves 8923 nn0n0n1ge2 9089 ixxssixx 9653 sumtp 11151 dvdsmulcr 11450 dvds2add 11454 dvds2sub 11455 dvdstr 11457 bj-peano4 13080 |
Copyright terms: Public domain | W3C validator |